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