P. 35 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3401-3500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rmoeq1 3401*	Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2147. (Revised by Wolf Lammen, 12-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	reueq1 3402*	Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2147. (Revised by Wolf Lammen, 12-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑))
Theorem	rmoeqd 3403*	Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	reueqd 3404*	Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	reueqdv 3405*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	reueqbidv 3406*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reubidv 3386. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒))
Theorem	rmoeq1f 3407	Equality theorem for restricted at-most-one quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	reueq1f 3408	Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑))
Theorem	cbvreu 3409*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvreuw 3396 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmo 3410*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrmow 3395, cbvrmovw 3391 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmov 3411*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuv 3412*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. See cbvreuvw 3392 for a version without ax-13 2406, but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvreuvw 3392 when possible. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmod 3413	Deduction version of nfrmo 3415. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓)
Theorem	nfreud 3414	Deduction version of nfreu 3416. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmo 3415	Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfrmow 3399 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreu 3416	Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfreuw 3400 when possible. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑
2.1.5.3  Restricted class abstraction
Syntax	crab 3417	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-rab 3418	Define a restricted class abstraction (class builder): {𝑥 ∈ 𝐴 ∣ 𝜑} is the class of all sets 𝑥 in 𝐴 such that 𝜑(𝑥) is true. Definition of [TakeutiZaring] p. 20. For the interpretation given in the previous paragraph to be correct, we need to assume Ⅎ𝑥𝐴, which is the case as soon as 𝑥 and 𝐴 are disjoint, which is generally the case. If 𝐴 were to depend on 𝑥, then the interpretation would be less obvious (think of the two extreme cases 𝐴 = {𝑥} and 𝐴 = 𝑥, for instance). See also df-ral 3080. (Contributed by NM, 22-Nov-1994.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	rabbidva2 3419*	Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbia2 3420	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}
Theorem	rabbiia 3421	Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbii 3422	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3424. (Contributed by Peter Mazsa, 1-Nov-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbidva 3423*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbidv 3424*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbieq 3425	Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabswap 3426	Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
Theorem	cbvrabv 3427*	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2194 and ax-13 2406. (Revised by Steven Nguyen, 4-Dec-2022.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	rabeqcda 3428*	When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3429. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴)
Theorem	rabeqc 3429*	A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022.) (Proof shortened by SN, 15-Jan-2025.)
⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = 𝐴
Theorem	rabeqi 3430	Equality theorem for restricted class abstractions. Inference form of rabeqf 3451. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2178, ax-11 2194, ax-12 2215. (Revised by GG, 3-Jun-2024.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	rabeq 3431*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2178, ax-11 2194, ax-12 2215. (Revised by GG, 20-Aug-2023.)
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	rabeqdv 3432*	Equality of restricted class abstractions. Deduction form of rabeq 3431. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	rabeqbidva 3433*	Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove DV conditions. (Revised by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeqbidvaOLD 3434*	Obsolete version of rabeqbidva 3433 as of 1-Sep-2025. (Contributed by Mario Carneiro, 26-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeqbidv 3435*	Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabrabi 3436*	Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2178, ax-11 2194 and ax-12 2215. (Revised by GG, 12-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))    ⇒   ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)}
Theorem	nfrab1 3437	The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}
Theorem	rabid 3438	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	rabidim1 3439	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)
Theorem	reqabi 3440	Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	rabrab 3441	Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	rabbida4 3442	Version of rabbidva2 3419 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbida 3443	Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva 3423 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) Avoid ax-10 2178, ax-11 2194. (Revised by Wolf Lammen, 14-Mar-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbid 3444	Version of rabbidv 3424 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabeqd 3445	Deduction form of rabeq 3431. Note that contrary to rabeq 3431 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	rabeqbida 3446	Version of rabeqbidva 3433 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbi 3447	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3422. (Contributed by NM, 25-Nov-2013.)
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabid2f 3448	An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rabid2im 3449*	One direction of rabid2 3450 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	rabid2 3450*	An "identity" law for restricted class abstraction. Prefer rabid2im 3449 if one direction is sufficient. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2024.)
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rabeqf 3451	Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	cbvrabw 3452*	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3456 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2178. (Revised by Wolf Lammen, 19-Jul-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	cbvrabwOLD 3453*	Obsolete version of cbvrabw 3452 as of 19-Jul-2025. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	nfrabw 3454*	A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3455 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	nfrab 3455	A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfrabw 3454 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	cbvrab 3456	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrabw 3452 when possible. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
2.1.6  The universal class
Syntax	cvv 3457	Extend class notation to include the universal class symbol.
class V
Theorem	vjust 3458	Justification theorem for df-v 3459. (Contributed by Rodolfo Medina, 27-Apr-2010.)
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦}
Definition	df-v 3459	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. The class V can be described as the "class of all sets"; vprc 5275 proves that V is not itself a set in ZF. We will frequently use the expression 𝐴 ∈ V as a short way to say "𝐴 is a set", and isset 3471 proves that this expression has the same meaning as ∃𝑥𝑥 = 𝐴. In well-founded set theories without urelements, like ZF, the class V is equal to the von Neumann universe. However, the letter "V" does not stand for "von Neumann". The letter "V" was used earlier by Peano in 1889 for the universe of sets, where the letter V is derived from the Latin word "Verum", referring to the true truth constant 𝑇. Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910. The class constant V is the first class constant introduced in this database. As a constant, as opposed to a variable, it cannot be substituted with anything, and in particular it is not part of any disjoint variable condition. For a general discussion of the theory of classes, see mmset.html#class 3471. See dfv2 3460 for an alternate definition. (Contributed by NM, 26-May-1993.)
⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
Theorem	dfv2 3460	Alternate definition of the universal class (see df-v 3459). (Contributed by BJ, 30-Nov-2019.)
⊢ V = {𝑥 ∣ ⊤}
Theorem	vex 3461	All setvar variables are sets (see isset 3471). Theorem 6.8 of [Quine] p. 43. A shorter proof is possible from eleq2i 2857 but it uses more axioms. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2215. (Revised by SN, 28-Aug-2023.) (Proof shortened by BJ, 4-Sep-2024.)
⊢ 𝑥 ∈ V
Theorem	elv 3462	If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3461), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ (𝑥 ∈ V → 𝜑)    ⇒   ⊢ 𝜑
Theorem	elvd 3463	If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3461) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3462. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el2v 3464	If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3461), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)    ⇒   ⊢ 𝜑
Theorem	el3v 3465	If a proposition is implied by 𝑥 ∈ V, 𝑦 ∈ V and 𝑧 ∈ V (which is true, see vex 3461), then it is true. Inference forms (with ⊢ 𝐴 ∈ V, ⊢ 𝐵 ∈ V and ⊢ 𝐶 ∈ V hypotheses) of the general theorems (proving ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → assertions) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜑)    ⇒   ⊢ 𝜑
Theorem	el3v3 3466	If a proposition is implied by 𝑧 ∈ V (which is true, see vex 3461) and two other antecedents, then it is implied by these other antecedents. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	eqv 3467*	The universe contains every set. (Contributed by NM, 11-Sep-2006.) Remove dependency on ax-10 2178, ax-11 2194, ax-13 2406. (Revised by BJ, 10-Aug-2022.)
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	eqvf 3468	The universe contains every set. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	abv 3469	The class of sets verifying a property is the universal class if and only if that property is a tautology. The reverse implication (bj-abv 37403) requires fewer axioms. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2840, ax-8 2147. (Revised by GG, 30-Aug-2024.) (Proof shortened by BJ, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑)
Theorem	abvALT 3470	Alternate proof of abv 3469, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑)
Theorem	isset 3471*	Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3459) if and only if the class 𝐴 exists (i.e., there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43. A class 𝐴 which is not a set is called a proper class. Conventions: We will often use the expression "𝐴 ∈ V " to mean "𝐴 is a set", for example in uniex 7728. To make some theorems more readily applicable, we will also use the more general expression 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg 7727 compared with uniex 7728). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3478. (Contributed by NM, 26-May-1993.)
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	cbvexeqsetf 3472*	The expression ∃𝑥𝑥 = 𝐴 means "𝐴 is a set" even if 𝐴 contains 𝑥 as a bound variable. This lemma helps minimizing axiom or df-clab 2744 usage in some cases. Extracted from the proof of issetft 3473. (Contributed by Wolf Lammen, 30-Jul-2025.)
⊢ (Ⅎ𝑥𝐴 → (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	issetft 3473	Closed theorem form of isset 3471 that does not require 𝑥 and 𝐴 to be distinct. Extracted from the proof of vtoclgft 3523. (Contributed by Wolf Lammen, 9-Apr-2025.)
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴))
Theorem	issetf 3474	A version of isset 3471 that does not require 𝑥 and 𝐴 to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	isseti 3475*	A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	issetri 3476*	A way to say "𝐴 is a set" (inference form). (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑥 𝑥 = 𝐴    ⇒   ⊢ 𝐴 ∈ V
Theorem	eqvisset 3477	A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 3471 and issetri 3476. (Contributed by BJ, 27-Apr-2019.)
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
Theorem	elex 3478	If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 28-May-2025.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
Theorem	elexi 3479	If a class is a member of another class, then it is a set. Inference associated with elex 3478. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	elexd 3480	If a class is a member of another class, then it is a set. Deduction associated with elex 3478. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	elex22 3481*	If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
Theorem	prcnel 3482	A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by AV, 14-Nov-2020.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 ∈ 𝑉)
Theorem	ralv 3483	A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑)
Theorem	rexv 3484	An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Theorem	reuv 3485	A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.)
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑)
Theorem	rmov 3486	An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑)
Theorem	rabab 3487	A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	rexcom4b 3488*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	ceqsal1t 3489	One direction of ceqsalt 3490 is based on fewer assumptions and fewer axioms. It is at the same time the reverse direction of vtoclgft 3523. Extracted from a proof of ceqsalt 3490. (Contributed by Wolf Lammen, 25-Mar-2025.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))
Theorem	ceqsalt 3490*	Closed theorem version of ceqsalg 3492. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsralt 3491*	Restricted quantifier version of ceqsalt 3490. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalg 3492*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. For an alternate proof, see ceqsalgALT 3493. (Contributed by NM, 29-Oct-2003.) (Proof shortened by BJ, 29-Sep-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalgALT 3493*	Alternate proof of ceqsalg 3492, not using ceqsalt 3490. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by BJ, 29-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsal 3494*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid df-clab 2744. (Revised by Wolf Lammen, 23-Jan-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalALT 3495*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. Shorter proof uses df-clab 2744. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalv 3496*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid ax-12 2215. (Revised by SN, 8-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsralv 3497*	Restricted quantifier version of ceqsalv 3496. (Contributed by NM, 21-Jun-2013.) Avoid ax-9 2155, ax-12 2215, ax-ext 2737. (Revised by SN, 8-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	gencl 3498*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵))    &   ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	2gencl 3499*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶)    &   ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷)    &   ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒)
Theorem	3gencl 3500*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷)    &   ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹)    &   ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺)    &   ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒))    &   ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃)