P. 382 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	igenss 38101	A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆))
Theorem	igenidl 38102	The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅))
Theorem	igenmin 38103	The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼)
Theorem	igenidl2 38104	The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼)
Theorem	igenval2 38105*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗))))
Theorem	prnc 38106*	A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
Theorem	isfldidl 38107	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	isfldidl2 38108	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑋 ≠ {𝑍} ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	ispridlc 38109*	The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
Theorem	pridlc 38110	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃))
Theorem	pridlc2 38111	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃)
Theorem	pridlc3 38112	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃))
Theorem	isdmn3 38113*	The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))
Theorem	dmnnzd 38114	A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍))
Theorem	dmncan1 38115	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶))
Theorem	dmncan2 38116	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐶 ≠ 𝑍) → ((𝐴𝐻𝐶) = (𝐵𝐻𝐶) → 𝐴 = 𝐵))
21.25  Mathbox for Giovanni Mascellani
21.25.1  Tools for automatic proof building The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings.
Theorem	efald2 38117	A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ 𝜑 → ⊥)    ⇒   ⊢ 𝜑
Theorem	notbinot1 38118	Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓))
Theorem	bicontr 38119	Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥)
Theorem	impor 38120	An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	orfa 38121	The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑)
Theorem	notbinot2 38122	Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓))
Theorem	biimpor 38123	A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒))
Theorem	orfa1 38124	Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ ⊥) → 𝜓)
Theorem	orfa2 38125	Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ ((𝜑 ∨ 𝜓) → 𝜓)
Theorem	bifald 38126	Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ ⊥))
Theorem	orsild 38127	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	orsird 38128	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	cnf1dd 38129	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnf2dd 38130	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	cnfn1dd 38131	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnfn2dd 38132	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	or32dd 38133	A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃)))
Theorem	notornotel1 38134	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	notornotel2 38135	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	contrd 38136	A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	an12i 38137	An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.)
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒))
Theorem	exmid2 38138	An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ ((𝜓 ∧ 𝜑) → 𝜒)    &   ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜂) → 𝜒)
Theorem	selconj 38139	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒)))
Theorem	truconj 38140	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
Theorem	orel 38141	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ ((𝜓 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜌) → 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃)
Theorem	negel 38142	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⊥)
Theorem	botel 38143	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	tradd 38144	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ (⊤ ∧ 𝜓))
Theorem	gm-sbtru 38145	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤)
Theorem	sbfal 38146	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥)
Theorem	sbcani 38147	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂))
Theorem	sbcori 38148	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂))
Theorem	sbcimi 38149	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂))
Theorem	sbcni 38150	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓)
Theorem	sbali 38151	Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbexi 38152	Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	sbcalf 38153*	Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcexf 38154*	Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcalfi 38155*	Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓)
Theorem	sbcexfi 38156*	Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓)
Theorem	spsbcdi 38157	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑥𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	alrimii 38158*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	spesbcdi 38159	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	exlimddvf 38160	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	exlimddvfi 38161	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑦𝜃    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂)    &   ⊢ ((𝜂 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	sbceq1ddi 38162	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃)    &   ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	sbccom2lem 38163*	Lemma for sbccom2 38164. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2 38164*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2f 38165*	Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2fi 38166*	Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓)
Theorem	csbcom2fi 38167*	Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸
21.25.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 38168	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ¬ ⊥)
Theorem	tsim1 38169	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓)))
Theorem	tsim2 38170	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓)))
Theorem	tsim3 38171	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓)))
Theorem	tsbi1 38172	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi2 38173	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 38174	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 38175	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 38176	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 38177	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 38178	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 38179	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 38180	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 38181	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 38182	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 38183	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 38184	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 38185	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 38186	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 38187	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 38188	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 38189	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 38190	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 38191	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 38192	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 38193	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 38194	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜒 ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
21.25.3  Equality deductions A collection of theorems for commuting equalities (or biconditionals) with other constructs.
Theorem	iuneq2f 38195	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 38196	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 38197	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 38198	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 38199	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 38200	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})