P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbccom2 33601*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2f 33602*	Commutative law for double class substitution, with non free variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2fi 33603*	Commutative law for double class substitution, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓)
Theorem	sbcgfi 33604	Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑)
Theorem	csbcom2fi 33605*	Commutative law for double class substitution in a class, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸
Theorem	csbgfi 33606	Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵
20.20.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 33607	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ¬ ⊥)
Theorem	tsim1 33608	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓)))
Theorem	tsim2 33609	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓)))
Theorem	tsim3 33610	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓)))
Theorem	tsbi1 33611	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi2 33612	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 33613	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 33614	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 33615	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 33616	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 33617	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 33618	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 33619	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 33620	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 33621	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 33622	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 33623	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 33624	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 33625	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 33626	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 33627	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 33628	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 33629	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 33630	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 33631	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 33632	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 33633	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜒 ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
20.20.3  Equality deductions A collection of theorems for commuting equalities (or biimplications) with other constructs.
Theorem	iuneq2f 33634	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	abeq12 33635	Equality deduction for class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	rabeq12f 33636	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 33637	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	nfbii2 33638	Equality deduction for not-freeness. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	sbeqi 33639	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 33640	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 33641	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpt2bi123f 33642*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 33643	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 33644	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 33645	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 33646	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐷 = 𝐸) → (𝑥 ∈ 𝐴 ↦ 𝐷) = (𝑥 ∈ 𝐵 ↦ 𝐸))
20.20.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	scottexf 33647*	A version of scottex 8708 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 33648*	A version of scott0 8709 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 33649*	A version of scott0f 33648 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 33650*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 33651*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Theorem	ac6s6f 33652*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
20.21  Mathbox for Rodolfo Medina
20.21.1  Partitions
Theorem	prtlem60 33653	Lemma for prter3 33686. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 33654	Commute two sides of a biconditional in a deduction. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜒)))
Theorem	jca2 33655	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca2r 33656	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 33657	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 33658	Lemma for prter3 33686: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 33659	Reverse of ibd 258. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	pm5.31r 33660	Variant of pm5.31 611. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
Theorem	2r19.29 33661	Double the quantifiers of theorem r19.29. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
Theorem	prtlem100 33662	Lemma for prter3 33686. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 33663*	Lemma for prter1 33683, prter2 33685, prter3 33686 and prtex 33684. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 33664	Lemma for prter2 33685. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	n0el 33665*	Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥)
Theorem	brabsb2 33666*	A closed form of brabsb 4956. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
Theorem	eqbrrdv2 33667*	Other version of eqbrrdiv 5189. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 33668*	Lemma for prter3 33686. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 33669*	Lemma for prter3 33686. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 33670	Lemma for prter2 33685. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 33671*	Lemma for prtex 33684 and prter3 33686. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 33672*	Lemma for prter1 33683, prter2 33685, prter3 33686 and prtex 33684. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 33673*	Lemma for prtex 33684, prter2 33685 and prter3 33686. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 33674*	Lemma for prter2 33685 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 33675	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 33676*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 33677	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 33678*	Lemma for prter1 33683, prter2 33685 and prtex 33684. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 33679*	Lemma for prter1 33683 and prtex 33684. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 33680*	Lemma for prter2 33685. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 33681*	Lemma for prter2 33685. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 33682*	Lemma for prter2 33685. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 33683*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 33684*	The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V))
Theorem	prter2 33685*	The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → (∪ 𝐴 / ∼ ) = (𝐴 ∖ {∅}))
Theorem	prter3 33686*	For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ((𝑆 Er ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆)
20.22  Mathbox for Norm Megill Note: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 33791, means that the definition or theorem is not used for the derivation of hlathil 36772. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 36772.
20.22.1  Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16 These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2051, axc7 2128, axc10 2251, axc11 2313, axc11n 2306, axc15 2302, axc9 2301, axc14 2371, and axc16 2131.
Axiom	ax-c5 33687	Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all 𝑥, it is true for any specific 𝑥 (that would typically occur as a free variable in the wff substituted for 𝜑). (A free variable is one that does not occur in the scope of a quantifier: 𝑥 and 𝑦 are both free in 𝑥 = 𝑦, but only 𝑥 is free in ∀𝑦𝑥 = 𝑦.) Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1719. Conditional forms of the converse are given by ax-13 2245, ax-c14 33695, ax-c16 33696, and ax-5 1836. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 2352. An interesting alternate axiomatization uses axc5c711 33722 and ax-c4 33688 in place of ax-c5 33687, ax-4 1734, ax-10 2016, and ax-11 2031. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 2051. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 33688	Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying 𝜓. Notice that 𝑥 must not be a free variable in the antecedent of the quantified implication, and we express this by binding 𝜑 to "protect" the axiom from a 𝜑 containing a free 𝑥. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69. This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 2126. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 33689	Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use axc5c711 33722 in place of ax-c5 33687, ax-c7 33689, and ax-11 2031. This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 2128. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 33690	A variant of ax6 2250. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is obsolete and should no longer be used. It is proved above as theorem axc10 2251. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 33691	Axiom ax-c11 33691 was the original version of ax-c11n 33692 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 33692 could replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). This axiom is obsolete and should no longer be used. It is proved above as theorem axc11 2313. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 33692	Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). The original version of this axiom was ax-c11 33691 and was replaced with this shorter ax-c11n 33692 ("n" for "new") in May 2008. The old axiom is proved from this one as theorem axc11 2313. Conversely, this axiom is proved from ax-c11 33691 as theorem axc11nfromc11 33730. This axiom was proved redundant in July 2015. See theorem axc11n 2306. This axiom is obsolete and should no longer be used. It is proved above as theorem axc11n 2306. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 33693	Axiom ax-c15 33693 was the original version of ax-12 2044, before it was discovered (in Jan. 2007) that the shorter ax-12 2044 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. To understand this theorem more easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning "if 𝑥 and 𝑦 are distinct variables then..." The antecedent becomes false if the same variable is substituted for 𝑥 and 𝑦, ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor." Interestingly, if the wff expression substituted for 𝜑 contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-c15 33693 (from which the ax-12 2044 instance follows by theorem ax12 2303.) The proof is by induction on formula length, using ax12eq 33745 and ax12el 33746 for the basis steps and ax12indn 33747, ax12indi 33748, and ax12inda 33752 for the induction steps. (This paragraph is true provided we use ax-c11 33691 in place of ax-c11n 33692.) This axiom is obsolete and should no longer be used. It is proved above as theorem axc15 2302, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 33694	Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever 𝑧 is distinct from 𝑥 and 𝑦, and 𝑥 = 𝑦 is true, then 𝑥 = 𝑦 quantified with 𝑧 is also true. In other words, 𝑧 is irrelevant to the truth of 𝑥 = 𝑦. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. This axiom is obsolete and should no longer be used. It is proved above as theorem axc9 2301. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 33695	Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-5 1836; see theorem axc14 2371. Alternately, ax-5 1836 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1836. We retain ax-c14 33695 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1836, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 2371. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 33696*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1836 to be a metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 4827), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1836; see theorem axc16 2131. Alternately, ax-5 1836 becomes logically redundant in the presence of this axiom, but without ax-5 1836 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 33696 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1836, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc16 2131. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
20.22.2  Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old Theorems ax12fromc15 33709 and ax13fromc9 33710 require some intermediate theorems that are included in this section.
Theorem	axc5 33697	This theorem repeats sp 2051 under the name axc5 33697, so that the metamath program's "verify markup" command will check that it matches axiom scheme ax-c5 33687. It is preferred that references to this theorem use the name sp 2051. (Contributed by NM, 18-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 33698	Rederivation of axiom ax-4 1734 from ax-c4 33688, ax-c5 33687, ax-gen 1719 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2126 for the derivation of ax-c4 33688 from ax-4 1734. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	ax10fromc7 33699	Rederivation of axiom ax-10 2016 from ax-c7 33689, ax-c4 33688, ax-c5 33687, ax-gen 1719 and propositional calculus. See axc7 2128 for the derivation of ax-c7 33689 from ax-10 2016. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 33700	Rederivation of axiom ax-6 1885 from ax-c7 33689, ax-c10 33690, ax-gen 1719 and propositional calculus. See axc10 2251 for the derivation of ax-c10 33690 from ax-6 1885. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦