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	nfrmow 3401*	Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3417 with a disjoint variable condition, which does not require ax-13 2407. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2407. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2156, ax-ext 2738. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreuw 3402*	Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3418 with a disjoint variable condition, which does not require ax-13 2407. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2407. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2156, ax-ext 2738. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑
Theorem	rmoeq1 3403*	Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2179, ax-11 2195, and ax-12 2216. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2148. (Revised by Wolf Lammen, 12-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	reueq1 3404*	Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2179, ax-11 2195, and ax-12 2216. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2148. (Revised by Wolf Lammen, 12-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑))
Theorem	rmoeqd 3405*	Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	reueqd 3406*	Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	reueqdv 3407*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	reueqbidv 3408*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reubidv 3388. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒))
Theorem	rmoeq1f 3409	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 3410	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 3411*	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 2407. Use the weaker cbvreuw 3398 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmo 3412*	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 2407. Use the weaker cbvrmow 3397, cbvrmovw 3393 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmov 3413*	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 2407. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuv 3414*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. See cbvreuvw 3394 for a version without ax-13 2407, but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2407. Use the weaker cbvreuvw 3394 when possible. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmod 3415	Deduction version of nfrmo 3417. Usage of this theorem is discouraged because it depends on ax-13 2407. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓)
Theorem	nfreud 3416	Deduction version of nfreu 3418. Usage of this theorem is discouraged because it depends on ax-13 2407. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmo 3417	Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2407. Use the weaker nfrmow 3401 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreu 3418	Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2407. Use the weaker nfreuw 3402 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 3419	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-rab 3420	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 3083. (Contributed by NM, 22-Nov-1994.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	rabbidva2 3421*	Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbia2 3422	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}
Theorem	rabbiia 3423	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 3424	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3426. (Contributed by Peter Mazsa, 1-Nov-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbidva 3425*	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 3426*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbieq 3427	Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabswap 3428	Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
Theorem	cbvrabv 3429*	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 2195 and ax-13 2407. (Revised by Steven Nguyen, 4-Dec-2022.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	rabeqcda 3430*	When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3431. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴)
Theorem	rabeqc 3431*	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 3432	Equality theorem for restricted class abstractions. Inference form of rabeqf 3453. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2179, ax-11 2195, ax-12 2216. (Revised by GG, 3-Jun-2024.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	rabeq 3433*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2179, ax-11 2195, ax-12 2216. (Revised by GG, 20-Aug-2023.)
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	rabeqdv 3434*	Equality of restricted class abstractions. Deduction form of rabeq 3433. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	rabeqbidva 3435*	Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove DV conditions. (Revised by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeqbidvaOLD 3436*	Obsolete version of rabeqbidva 3435 as of 1-Sep-2025. (Contributed by Mario Carneiro, 26-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeqbidv 3437*	Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabrabi 3438*	Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2179, ax-11 2195 and ax-12 2216. (Revised by GG, 12-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))    ⇒   ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)}
Theorem	nfrab1 3439	The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}
Theorem	rabid 3440	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 3441	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)
Theorem	reqabi 3442	Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	rabrab 3443	Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	rabbida4 3444	Version of rabbidva2 3421 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbida 3445	Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva 3425 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) Avoid ax-10 2179, ax-11 2195. (Revised by Wolf Lammen, 14-Mar-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbid 3446	Version of rabbidv 3426 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabeqd 3447	Deduction form of rabeq 3433. Note that contrary to rabeq 3433 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	rabeqbida 3448	Version of rabeqbidva 3435 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbi 3449	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3424. (Contributed by NM, 25-Nov-2013.)
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabid2f 3450	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 3451*	One direction of rabid2 3452 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	rabid2 3452*	An "identity" law for restricted class abstraction. Prefer rabid2im 3451 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 3453	Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	cbvrabw 3454*	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3457 with a disjoint variable condition, which does not require ax-13 2407. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2407. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2179. (Revised by Wolf Lammen, 19-Jul-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	nfrabw 3455*	A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3456 with a disjoint variable condition, which does not require ax-13 2407. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2407. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	nfrab 3456	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 2407. Use the weaker nfrabw 3455 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	cbvrab 3457	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 2407. Use the weaker cbvrabw 3454 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 3458	Extend class notation to include the universal class symbol.
class V
Theorem	vjust 3459	Justification theorem for df-v 3460. (Contributed by Rodolfo Medina, 27-Apr-2010.)
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦}
Definition	df-v 3460	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 5288 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 3472 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 3472. See dfv2 3461 for an alternate definition. (Contributed by NM, 26-May-1993.)
⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
Theorem	dfv2 3461	Alternate definition of the universal class (see df-v 3460). (Contributed by BJ, 30-Nov-2019.)
⊢ V = {𝑥 ∣ ⊤}
Theorem	vex 3462	All setvar variables are sets (see isset 3472). Theorem 6.8 of [Quine] p. 43. A shorter proof is possible from eleq2i 2858 but it uses more axioms. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2216. (Revised by SN, 28-Aug-2023.) (Proof shortened by BJ, 4-Sep-2024.)
⊢ 𝑥 ∈ V
Theorem	elv 3463	If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3462), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ (𝑥 ∈ V → 𝜑)    ⇒   ⊢ 𝜑
Theorem	elvd 3464	If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3462) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3463. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el2v 3465	If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3462), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)    ⇒   ⊢ 𝜑
Theorem	el3v 3466	If a proposition is implied by 𝑥 ∈ V, 𝑦 ∈ V and 𝑧 ∈ V (which is true, see vex 3462), 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 3467	If a proposition is implied by 𝑧 ∈ V (which is true, see vex 3462) and two other antecedents, then it is implied by these other antecedents. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	eqv 3468*	The universe contains every set. (Contributed by NM, 11-Sep-2006.) Remove dependency on ax-10 2179, ax-11 2195, ax-13 2407. (Revised by BJ, 10-Aug-2022.)
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	eqvf 3469	The universe contains every set. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	abv 3470	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 37581) requires fewer axioms. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2841, ax-8 2148. (Revised by GG, 30-Aug-2024.) (Proof shortened by BJ, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑)
Theorem	abvALT 3471	Alternate proof of abv 3470, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑)
Theorem	isset 3472*	Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3460) 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 7752. 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 7751 compared with uniex 7752). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3479. (Contributed by NM, 26-May-1993.)
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	cbvexeqsetf 3473*	The expression ∃𝑥𝑥 = 𝐴 means "𝐴 is a set" even if 𝐴 contains 𝑥 as a bound variable. This lemma helps minimizing axiom or df-clab 2745 usage in some cases. Extracted from the proof of issetft 3474. (Contributed by Wolf Lammen, 30-Jul-2025.)
⊢ (Ⅎ𝑥𝐴 → (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	issetft 3474	Closed theorem form of isset 3472 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 3475	A version of isset 3472 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 3476*	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 3477*	A way to say "𝐴 is a set" (inference form). (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑥 𝑥 = 𝐴    ⇒   ⊢ 𝐴 ∈ V
Theorem	eqvisset 3478	A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 3472 and issetri 3477. (Contributed by BJ, 27-Apr-2019.)
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
Theorem	elex 3479	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 3480	If a class is a member of another class, then it is a set. Inference associated with elex 3479. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	elexd 3481	If a class is a member of another class, then it is a set. Deduction associated with elex 3479. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	elex22 3482*	If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
Theorem	prcnel 3483	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 3484	A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑)
Theorem	rexv 3485	An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Theorem	reuv 3486	A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.)
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑)
Theorem	rmov 3487	An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑)
Theorem	rabab 3488	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 3489*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	ceqsal1t 3490	One direction of ceqsalt 3491 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 3491. (Contributed by Wolf Lammen, 25-Mar-2025.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))
Theorem	ceqsalt 3491*	Closed theorem version of ceqsalg 3493. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsralt 3492*	Restricted quantifier version of ceqsalt 3491. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalg 3493*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. For an alternate proof, see ceqsalgALT 3494. (Contributed by NM, 29-Oct-2003.) (Proof shortened by BJ, 29-Sep-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalgALT 3494*	Alternate proof of ceqsalg 3493, not using ceqsalt 3491. (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 3495*	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 2745. (Revised by Wolf Lammen, 23-Jan-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalALT 3496*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. Shorter proof uses df-clab 2745. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalv 3497*	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 2216. (Revised by SN, 8-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsralv 3498*	Restricted quantifier version of ceqsalv 3497. (Contributed by NM, 21-Jun-2013.) Avoid ax-9 2156, ax-12 2216, ax-ext 2738. (Revised by SN, 8-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	gencl 3499*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵))    &   ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	2gencl 3500*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶)    &   ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷)    &   ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒)