P. 351 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35001-35100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fz0n 35001	The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
Theorem	shftvalg 35002	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	divcnvlin 35003*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	climlec3 35004*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	logi 35005	Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (log‘i) = (i · (π / 2))
Theorem	iexpire 35006	i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (i↑𝑐i) ∈ ℝ
Theorem	bcneg1 35007	The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0)
Theorem	bcm1nt 35008	The proportion of one bionmial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾))))
Theorem	bcprod 35009*	A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))
Theorem	bccolsum 35010*	A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1)))
21.10.6  Infinite products
Theorem	iprodefisumlem 35011	Lemma for iprodefisum 35012. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹)))
Theorem	iprodefisum 35012*	Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵))
Theorem	iprodgam 35013*	An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴))
21.10.7  Factorial limits
Theorem	faclimlem1 35014*	Lemma for faclim 35017. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))
Theorem	faclimlem2 35015*	Lemma for faclim 35017. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1))
Theorem	faclimlem3 35016	Lemma for faclim 35017. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵)))))
Theorem	faclim 35017*	An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))    ⇒   ⊢ (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴))
Theorem	iprodfac 35018*	An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘))))
Theorem	faclim2 35019*	Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀))))    ⇒   ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1)
21.10.8  Greatest common divisor and divisibility
Theorem	gcd32 35020	Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = ((𝐴 gcd 𝐶) gcd 𝐵))
Theorem	gcdabsorb 35021	Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵))
21.10.9  Properties of relationships
Theorem	dftr6 35022	A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E )))
Theorem	coep 35023*	Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥)
Theorem	coepr 35024*	Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵)
Theorem	dffr5 35025	A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅)))
Theorem	dfso2 35026	Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))))
Theorem	br8 35027*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)}    ⇒   ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Theorem	br6 35028*	Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Theorem	br4 35029*	Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))
Theorem	cnvco1 35030	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴)
Theorem	cnvco2 35031	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴)
Theorem	eldm3 35032	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)
Theorem	elrn3 35033	Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅)
Theorem	pocnv 35034	The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴)
Theorem	socnv 35035	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴)
Theorem	sotrd 35036	Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    &   ⊢ (𝜑 → 𝑌𝑅𝑍)    ⇒   ⊢ (𝜑 → 𝑋𝑅𝑍)
Theorem	elintfv 35037*	Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ 𝑋 ∈ V    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦)))
21.10.10  Properties of functions and mappings
Theorem	funpsstri 35038	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹))
Theorem	fundmpss 35039	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 35040	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 35041	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funbreq 35042	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶))
Theorem	br1steq 35043	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 35044	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 35045	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 35046	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 35047	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
Theorem	elima4 35048	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)
Theorem	fv1stcnv 35049	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	fv2ndcnv 35050	The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = ⟨𝑋, 𝑌⟩)
21.10.11  Set induction (or epsilon induction)
Theorem	setinds 35051*	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 35052*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2 35053*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
21.10.12  Ordinal numbers
Theorem	elpotr 35054*	A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.)
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴)
Theorem	dford5reg 35055	Given ax-reg 9590, 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 35056	Lemma for dfon2 35065. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)}
Theorem	dfon2lem2 35057*	Lemma for dfon2 35065. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴
Theorem	dfon2lem3 35058*	Lemma for dfon2 35065. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)))
Theorem	dfon2lem4 35059*	Lemma for dfon2 35065. 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 35060*	Lemma for dfon2 35065. 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 35061*	Lemma for dfon2 35065. 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 35062*	Lemma for dfon2 35065. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)))
Theorem	dfon2lem8 35063*	Lemma for dfon2 35065. 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 35064*	Lemma for dfon2 35065. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴)
Theorem	dfon2 35065*	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 35066	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 35067	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 35068*	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 35069*	Generalization of dfrdg2 35068 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.10.13  Defined equality axioms
Theorem	axextdfeq 35070	A version of ax-ext 2702 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)))
Theorem	ax8dfeq 35071	A version of ax-8 2107 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦))
Theorem	axextdist 35072	ax-ext 2702 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	axextbdist 35073	axextb 2705 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))
Theorem	19.12b 35074*	Version of 19.12vv 2342 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 35075	There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦
Theorem	distel 35076	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5438 and elirrv 9594.) (Contributed by Scott Fenton, 15-Dec-2010.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦)
Theorem	axextndbi 35077	axextnd 10589 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
21.10.14  Hypothesis builders
Theorem	hbntg 35078	A more general form of hbnt 2289. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))
Theorem	hbimtg 35079	A more general and closed form of hbim 2294. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃)))
Theorem	hbaltg 35080	A more general and closed form of hbal 2166. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	hbng 35081	A more general form of hbn 2290. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑)
Theorem	hbimg 35082	A more general form of hbim 2294. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃))
21.10.15  Well-founded zero, successor, and limits
Syntax	cwsuc 35083	Declare the syntax for well-founded successor.
class wsuc(𝑅, 𝐴, 𝑋)
Syntax	cwlim 35084	Declare the syntax for well-founded limit class.
class WLim(𝑅, 𝐴)
Definition	df-wsuc 35085	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 35086*	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 35087	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌))
Theorem	wsuceq1 35088	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋))
Theorem	wsuceq2 35089	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋))
Theorem	wsuceq3 35090	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌))
Theorem	nfwsuc 35091	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 35092	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵))
Theorem	wlimeq1 35093	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴))
Theorem	wlimeq2 35094	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵))
Theorem	nfwlim 35095	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 35096	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)))
Theorem	wzel 35097	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 35098*	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 35099	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 35100*	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(𝑅, 𝐴, 𝑋) ∈ 𝐴)