P. 357 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35601-35700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	coepr 35601*	Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵)
Theorem	dffr5 35602	A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅)))
Theorem	dfso2 35603	Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))))
Theorem	br8 35604*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)}    ⇒   ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Theorem	br6 35605*	Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Theorem	br4 35606*	Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))
Theorem	cnvco1 35607	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴)
Theorem	cnvco2 35608	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴)
Theorem	eldm3 35609	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)
Theorem	elrn3 35610	Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅)
Theorem	pocnv 35611	The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴)
Theorem	socnv 35612	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴)
Theorem	sotrd 35613	Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    &   ⊢ (𝜑 → 𝑌𝑅𝑍)    ⇒   ⊢ (𝜑 → 𝑋𝑅𝑍)
Theorem	elintfv 35614*	Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ 𝑋 ∈ V    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦)))
21.11.10  Properties of functions and mappings
Theorem	funpsstri 35615	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹))
Theorem	fundmpss 35616	If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺))
Theorem	funsseq 35617	Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺))
Theorem	fununiq 35618	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funbreq 35619	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶))
Theorem	br1steq 35620	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴)
Theorem	br2ndeq 35621	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵)
Theorem	dfdm5 35622	Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴)
Theorem	dfrn5 35623	Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴)
Theorem	opelco3 35624	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
Theorem	elima4 35625	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)
Theorem	fv1stcnv 35626	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	fv2ndcnv 35627	The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = ⟨𝑋, 𝑌⟩)
21.11.11  Set induction (or epsilon induction)
Theorem	setinds 35628*	Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2f 35629*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2 35630*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
21.11.12  Ordinal numbers
Theorem	elpotr 35631*	A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.)
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴)
Theorem	dford5reg 35632	Given ax-reg 9639, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴))
Theorem	dfon2lem1 35633	Lemma for dfon2 35642. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)}
Theorem	dfon2lem2 35634*	Lemma for dfon2 35642. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴
Theorem	dfon2lem3 35635*	Lemma for dfon2 35642. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)))
Theorem	dfon2lem4 35636*	Lemma for dfon2 35642. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	dfon2lem5 35637*	Lemma for dfon2 35642. Two sets satisfying the new definition also satisfy trichotomy with respect to ∈. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	dfon2lem6 35638*	Lemma for dfon2 35642. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
Theorem	dfon2lem7 35639*	Lemma for dfon2 35642. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)))
Theorem	dfon2lem8 35640*	Lemma for dfon2 35642. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))
Theorem	dfon2lem9 35641*	Lemma for dfon2 35642. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴)
Theorem	dfon2 35642*	On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}
Theorem	rdgprc0 35643	The value of the recursive definition generator at ∅ when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → (rec(𝐹, 𝐼)‘∅) = ∅)
Theorem	rdgprc 35644	The value of the recursive definition generator when 𝐼 is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → rec(𝐹, 𝐼) = rec(𝐹, ∅))
Theorem	dfrdg2 35645*	Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
Theorem	dfrdg3 35646*	Generalization of dfrdg2 35645 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐼 ∈ V, 𝐼, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
21.11.13  Defined equality axioms
Theorem	axextdfeq 35647	A version of ax-ext 2700 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)))
Theorem	ax8dfeq 35648	A version of ax-8 2102 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦))
Theorem	axextdist 35649	ax-ext 2700 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	axextbdist 35650	axextb 2703 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))
Theorem	19.12b 35651*	Version of 19.12vv 2341 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	exnel 35652	There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦
Theorem	distel 35653	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5444 and elirrv 9643.) (Contributed by Scott Fenton, 15-Dec-2010.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦)
Theorem	axextndbi 35654	axextnd 10638 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
21.11.14  Hypothesis builders
Theorem	hbntg 35655	A more general form of hbnt 2287. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))
Theorem	hbimtg 35656	A more general and closed form of hbim 2292. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃)))
Theorem	hbaltg 35657	A more general and closed form of hbal 2160. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	hbng 35658	A more general form of hbn 2288. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑)
Theorem	hbimg 35659	A more general form of hbim 2292. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃))
21.11.15  Well-founded zero, successor, and limits
Syntax	cwsuc 35660	Declare the syntax for well-founded successor.
class wsuc(𝑅, 𝐴, 𝑋)
Syntax	cwlim 35661	Declare the syntax for well-founded limit class.
class WLim(𝑅, 𝐴)
Definition	df-wsuc 35662	Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
Definition	df-wlim 35663*	Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
Theorem	wsuceq123 35664	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌))
Theorem	wsuceq1 35665	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋))
Theorem	wsuceq2 35666	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋))
Theorem	wsuceq3 35667	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌))
Theorem	nfwsuc 35668	Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    ⇒   ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋)
Theorem	wlimeq12 35669	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵))
Theorem	wlimeq1 35670	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴))
Theorem	wlimeq2 35671	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵))
Theorem	nfwlim 35672	Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥WLim(𝑅, 𝐴)
Theorem	elwlim 35673	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)))
Theorem	wzel 35674	The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴)
Theorem	wsuclem 35675*	Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦)))
Theorem	wsucex 35676	Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	wsuccl 35677*	If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴)
Theorem	wsuclb 35678	A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    ⇒   ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋))
Theorem	wlimss 35679	The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴
21.11.16  Quantifier-free definitions
Syntax	ctxp 35680	Declare the syntax for tail Cartesian product.
class (𝐴 ⊗ 𝐵)
Syntax	cpprod 35681	Declare the syntax for the parallel product.
class pprod(𝑅, 𝑆)
Syntax	csset 35682	Declare the subset relationship class.
class SSet
Syntax	ctrans 35683	Declare the transitive set class.
class Trans
Syntax	cbigcup 35684	Declare the set union relationship.
class Bigcup
Syntax	cfix 35685	Declare the syntax for the fixpoints of a class.
class Fix 𝐴
Syntax	climits 35686	Declare the class of limit ordinals.
class Limits
Syntax	cfuns 35687	Declare the syntax for the class of all function.
class Funs
Syntax	csingle 35688	Declare the syntax for the singleton function.
class Singleton
Syntax	csingles 35689	Declare the syntax for the class of all singletons.
class Singletons
Syntax	cimage 35690	Declare the syntax for the image functor.
class Image𝐴
Syntax	ccart 35691	Declare the syntax for the cartesian function.
class Cart
Syntax	cimg 35692	Declare the syntax for the image function.
class Img
Syntax	cdomain 35693	Declare the syntax for the domain function.
class Domain
Syntax	crange 35694	Declare the syntax for the range function.
class Range
Syntax	capply 35695	Declare the syntax for the application function.
class Apply
Syntax	ccup 35696	Declare the syntax for the cup function.
class Cup
Syntax	ccap 35697	Declare the syntax for the cap function.
class Cap
Syntax	csuccf 35698	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 35699	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 35700	Declare the syntax for the full function functor.
class FullFun𝐹