P. 32 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3101-3200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ralim 3101	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexim 3102	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ralbii2 3103	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexbii2 3104	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)
Theorem	ralbiia 3105	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbiia 3106	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralbii 3107	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 4-Dec-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbii 3108	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralanid 3109	Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexanid 3110	Cancellation law for restricted existential quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 8-Jul-2023.)
⊢ (∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	ralcom3 3111	A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))
Theorem	dfral2 3112	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3113. (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rexnal 3113	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralinexa 3114	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	rexanali 3115	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
Theorem	ralbi 3116	Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1837. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexbi 3117	Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ralrexbid 3118	Formula-building rule for restricted existential quantifier, using a restricted universal quantifier to bind the quantified variable in the antecedent. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃))
Theorem	r19.35 3119	Restricted quantifier version of 19.35 1896. (Contributed by NM, 20-Sep-2003.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.26m 3120	Version of 19.26 1889 and r19.26 3121 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.)
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	r19.26 3121	Restricted quantifier version of 19.26 1889. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.26-3 3122	Version of r19.26 3121 with three quantifiers. (Contributed by FL, 22-Nov-2010.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralbiim 3123	Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1908. (Contributed by NM, 3-Jun-2012.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)))
Theorem	r19.29 3124	Restricted quantifier version of 19.29 1892. See also r19.29r 3125. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29r 3125	Restricted quantifier version of 19.29r 1893; variation of r19.29 3124. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29imd 3126	Theorem 19.29 of [Margaris] p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))
Theorem	r19.40 3127	Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.30 3128	Restricted quantifier version of 19.30 1900. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.43 3129	Restricted quantifier version of 19.43 1901. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	3r19.43 3130	Restricted quantifier version of 19.43 1901 for a triple disjunction . (Contributed by AV, 2-Nov-2025.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	2ralimi 3131	Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	3ralimi 3132	Inference quantifying both antecedent and consequent three times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	4ralimi 3133	Inference quantifying both antecedent and consequent four times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓)
Theorem	5ralimi 3134	Inference quantifying both antecedent and consequent five times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜓)
Theorem	6ralimi 3135	Inference quantifying both antecedent and consequent six times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜓)
Theorem	2ralbii 3136	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	2rexbii 3137	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
Theorem	3ralbii 3138	Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	4ralbii 3139	Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓)
Theorem	2ralbiim 3140	Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim 1909 and ralbiim 3123. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜑)))
Theorem	ralnex2 3141	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	ralnex3 3142	Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.) (Proof shortened by Wolf Lammen, 18-May-2023.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑)
Theorem	rexnal2 3143	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑)
Theorem	rexnal3 3144	Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
Theorem	nrexralim 3145	Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009.)
⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ¬ 𝜓))
Theorem	r19.26-2 3146	Restricted quantifier version of 19.26-2 1890. Version of r19.26 3121 with two quantifiers. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
Theorem	2r19.29 3147	Theorem r19.29 3124 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
Theorem	r19.29d2r 3148	Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒))
Theorem	r2allem 3149	Lemma factoring out common proof steps of r2alf 3282 and r2al 3197. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.)
⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2exlem 3150	Lemma factoring out common proof steps in r2exf 3283 an r2ex 3198. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	hbralrimi 3151	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3259 and ralrimiv 3152. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimiv 3152*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimiva 3153*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexlimiva 3154*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimiv 3155*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	nrexdv 3156*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimivw 3157*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexlimivw 3158*	Weaker version of rexlimiv 3155. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	ralrimdv 3159*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexlimdv 3160*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	ralrimdva 3161*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexlimdva 3162*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvaa 3163*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdva2 3164*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	r19.29an 3165*	A commonly used pattern in the spirit of r19.29 3124. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)
Theorem	rexlimdv3a 3166*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3160. (Contributed by NM, 7-Jun-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvw 3167*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddv 3168*	Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	r19.29a 3169*	A commonly used pattern in the spirit of r19.29 3124. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ralimdv2 3170*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))
Theorem	reximdv2 3171*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))
Theorem	reximdvai 3172*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdva 3173*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	reximdva 3174*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdv 3175*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1829). (Contributed by NM, 8-Oct-2003.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	reximdv 3176*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	reximddv 3177*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	reximddv3 3178*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	reximssdv 3179*	Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	ralbidv2 3180*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexbidv2 3181*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	ralbidva 3182*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidva 3183*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidv 3184*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidv 3185*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	r19.21v 3186*	Restricted quantifier version of 19.21v 1958. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.37v 3187*	Restricted quantifier version of one direction of 19.37v 2016. (The other direction holds iff 𝐴 is nonempty, see r19.37zv 4460.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.23v 3188*	Restricted quantifier version of 19.23v 1961. Version of r19.23 3258 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	r19.36v 3189*	Restricted quantifier version of one direction of 19.36 2264. (The other direction holds iff 𝐴 is nonempty, see r19.36zv 4465.) (Contributed by NM, 22-Oct-2003.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	r19.27v 3190*	Restricted quantitifer version of one direction of 19.27 2261. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.27zv 4464.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.41v 3191*	Restricted quantifier version 19.41v 1968. Version of r19.41 3265 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
Theorem	r19.28v 3192*	Restricted quantifier version of one direction of 19.28 2262. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.28zv 4459.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.42v 3193*	Restricted quantifier version of 19.42v 1972 (see also 19.42 2270). (Contributed by NM, 27-May-1998.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.32v 3194*	Restricted quantifier version of 19.32v 1959. (Contributed by NM, 25-Nov-2003.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.45v 3195*	Restricted quantifier version of one direction of 19.45 2272. The other direction holds when 𝐴 is nonempty, see r19.45zv 4461. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.44v 3196*	One direction of a restricted quantifier version of 19.44 2271. The other direction holds when 𝐴 is nonempty, see r19.44zv 4462. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))
Theorem	r2al 3197*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2ex 3198*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	r3al 3199*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.) (Proof shortened by Wolf Lammen, 30-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))
Theorem	r3ex 3200*	Triple existential quantification. (Contributed by AV, 21-Jul-2025.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑥∃𝑦∃𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝜑))