P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axacprim 35701	ax-ac 10419 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))))))
21.11.2  Untangled classes
Theorem	untelirr 35702*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 35787). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴)
Theorem	untuni 35703*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥)
Theorem	untsucf 35704*	If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	unt0 35705	The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥
Theorem	untint 35706*	If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀𝑦 ∈ ∩ 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	efrunt 35707*	If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥)
Theorem	untangtr 35708*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦))
21.11.3  Extra propositional calculus theorems
Theorem	3jaodd 35709	Double deduction form of 3jaoi 1430. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂)))
Theorem	3orit 35710	Closed form of 3ori 1426. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	biimpexp 35711	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒)))
21.11.4  Misc. Useful Theorems
Theorem	nepss 35712	Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵))
Theorem	3ccased 35713	Triple disjunction form of ccased 1038. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))    ⇒   ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))
Theorem	dfso3 35714*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	brtpid1 35715	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
Theorem	brtpid2 35716	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
Theorem	brtpid3 35717	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
Theorem	iota5f 35718*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	jath 35719	Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))
Theorem	xpab 35720*	Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	nnuni 35721	The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω)
21.11.5  Properties of real and complex numbers
Theorem	sqdivzi 35722	Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
Theorem	supfz 35723	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
Theorem	inffz 35724	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
Theorem	fz0n 35725	The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
Theorem	shftvalg 35726	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	divcnvlin 35727*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	climlec3 35728*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	iexpire 35729	i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (i↑𝑐i) ∈ ℝ
Theorem	bcneg1 35730	The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0)
Theorem	bcm1nt 35731	The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾))))
Theorem	bcprod 35732*	A product identity for binomial coefficients. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))
Theorem	bccolsum 35733*	A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1)))
21.11.6  Infinite products
Theorem	iprodefisumlem 35734	Lemma for iprodefisum 35735. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹)))
Theorem	iprodefisum 35735*	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 35736*	An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴))
21.11.7  Factorial limits
Theorem	faclimlem1 35737*	Lemma for faclim 35740. 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 35738*	Lemma for faclim 35740. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1))
Theorem	faclimlem3 35739	Lemma for faclim 35740. 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 35740*	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 35741*	An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘))))
Theorem	faclim2 35742*	Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀))))    ⇒   ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1)
21.11.8  Greatest common divisor and divisibility
Theorem	gcd32 35743	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 35744	Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵))
21.11.9  Properties of relationships
Theorem	dftr6 35745	A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E )))
Theorem	coep 35746*	Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥)
Theorem	coepr 35747*	Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵)
Theorem	dffr5 35748	A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅)))
Theorem	dfso2 35749	Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))))
Theorem	br8 35750*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)}    ⇒   ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Theorem	br6 35751*	Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Theorem	br4 35752*	Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))
Theorem	cnvco1 35753	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴)
Theorem	cnvco2 35754	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴)
Theorem	eldm3 35755	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)
Theorem	elrn3 35756	Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅)
Theorem	pocnv 35757	The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴)
Theorem	socnv 35758	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴)
Theorem	elintfv 35759*	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 35760	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹))
Theorem	fundmpss 35761	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 35762	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 35763	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funbreq 35764	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶))
Theorem	br1steq 35765	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 35766	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 35767	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 35768	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 35769	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
Theorem	elima4 35770	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)
Theorem	fv1stcnv 35771	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	fv2ndcnv 35772	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 35773*	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 35774*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2 35775*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
21.11.12  Ordinal numbers
Theorem	elpotr 35776*	A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.)
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴)
Theorem	dford5reg 35777	Given ax-reg 9552, 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 35778	Lemma for dfon2 35787. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)}
Theorem	dfon2lem2 35779*	Lemma for dfon2 35787. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴
Theorem	dfon2lem3 35780*	Lemma for dfon2 35787. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)))
Theorem	dfon2lem4 35781*	Lemma for dfon2 35787. 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 35782*	Lemma for dfon2 35787. 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 35783*	Lemma for dfon2 35787. 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 35784*	Lemma for dfon2 35787. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)))
Theorem	dfon2lem8 35785*	Lemma for dfon2 35787. 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 35786*	Lemma for dfon2 35787. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴)
Theorem	dfon2 35787*	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 35788	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 35789	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 35790*	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 35791*	Generalization of dfrdg2 35790 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 35792	A version of ax-ext 2702 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)))
Theorem	ax8dfeq 35793	A version of ax-8 2111 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦))
Theorem	axextdist 35794	ax-ext 2702 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	axextbdist 35795	axextb 2705 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))
Theorem	19.12b 35796*	Version of 19.12vv 2345 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 35797	There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦
Theorem	distel 35798	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5400 and elirrv 9556.) (Contributed by Scott Fenton, 15-Dec-2010.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦)
Theorem	axextndbi 35799	axextnd 10551 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
21.11.14  Hypothesis builders
Theorem	hbntg 35800	A more general form of hbnt 2294. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))