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	ralanid 3101	Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexanid 3102	Cancellation law for restricted existential quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 8-Jul-2023.)
⊢ (∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	ralcom3 3103	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	ralcom3OLD 3104	Obsolete version of ralcom3 3103 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))
Theorem	dfral2 3105	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3106. (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rexnal 3106	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralinexa 3107	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	rexanali 3108	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
Theorem	ralbi 3109	Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1816. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexbi 3110	Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	rexbiOLD 3111	Obsolete version of rexbi 3110 as of 31-Oct-2024. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ralrexbid 3112	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	ralrexbidOLD 3113	Obsolete version of ralrexbid 3112 as of 4-Nov-2024. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃))
Theorem	r19.35 3114	Restricted quantifier version of 19.35 1876. (Contributed by NM, 20-Sep-2003.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.35OLD 3115	Obsolete version of 19.35 1876 as of 22-Dec-2024. (Contributed by NM, 20-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.26m 3116	Version of 19.26 1869 and r19.26 3117 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.)
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	r19.26 3117	Restricted quantifier version of 19.26 1869. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.26-3 3118	Version of r19.26 3117 with three quantifiers. (Contributed by FL, 22-Nov-2010.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralbiim 3119	Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1888. (Contributed by NM, 3-Jun-2012.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)))
Theorem	r19.29 3120	Restricted quantifier version of 19.29 1872. See also r19.29r 3122. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29OLD 3121	Obsolete version of r19.29 3120 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29r 3122	Restricted quantifier version of 19.29r 1873; variation of r19.29 3120. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29rOLD 3123	Obsolete version of r19.29r 3122 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.29imd 3124	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 3125	Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.30 3126	Restricted quantifier version of 19.30 1880. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.30OLD 3127	Obsolete version of 19.30 1880 as of 5-Nov-2024. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.43 3128	Restricted quantifier version of 19.43 1881. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	2ralimi 3129	Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	3ralimi 3130	Inference quantifying both antecedent and consequent three times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	4ralimi 3131	Inference quantifying both antecedent and consequent four times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓)
Theorem	5ralimi 3132	Inference quantifying both antecedent and consequent five times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜓)
Theorem	6ralimi 3133	Inference quantifying both antecedent and consequent six times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜓)
Theorem	2ralbii 3134	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	2rexbii 3135	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
Theorem	3ralbii 3136	Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	4ralbii 3137	Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓)
Theorem	2ralbiim 3138	Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim 1889 and ralbiim 3119. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜑)))
Theorem	ralnex2 3139	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 3140	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 3141	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑)
Theorem	rexnal3 3142	Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
Theorem	nrexralim 3143	Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009.)
⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ¬ 𝜓))
Theorem	r19.26-2 3144	Restricted quantifier version of 19.26-2 1870. Version of r19.26 3117 with two quantifiers. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
Theorem	2r19.29 3145	Theorem r19.29 3120 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
Theorem	r19.29d2r 3146	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	r19.29d2rOLD 3147	Obsolete version of r19.29d2r 3146 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 30-Jan-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒))
Theorem	r2allem 3148	Lemma factoring out common proof steps of r2alf 3287 and r2al 3201. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.)
⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2exlem 3149	Lemma factoring out common proof steps in r2exf 3288 an r2ex 3202. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	hbralrimi 3150	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3263 and ralrimiv 3151. 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 3151*	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 3152*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexlimiva 3153*	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 3154*	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 3155*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimivw 3156*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexlimivw 3157*	Weaker version of rexlimiv 3154. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	ralrimdv 3158*	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 3159*	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 3160*	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 3161*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvaa 3162*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdva2 3163*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	r19.29an 3164*	A commonly used pattern in the spirit of r19.29 3120. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)
Theorem	rexlimdv3a 3165*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3159. (Contributed by NM, 7-Jun-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvw 3166*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddv 3167*	Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	r19.29a 3168*	A commonly used pattern in the spirit of r19.29 3120. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ralimdv2 3169*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))
Theorem	reximdv2 3170*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))
Theorem	reximdvai 3171*	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	reximdvaiOLD 3172*	Obsolete version of reximdvai 3171 as of 3-Nov-2024. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
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 1808). (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 1938. (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.21vOLD 3187*	Obsolete version of r19.21v 3186 as of 11-Dec-2024. (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 modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.37v 3188*	Restricted quantifier version of one direction of 19.37v 1991. (The other direction holds iff 𝐴 is nonempty, see r19.37zv 4525.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.23v 3189*	Restricted quantifier version of 19.23v 1941. Version of r19.23 3262 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 3190*	Restricted quantifier version of one direction of 19.36 2231. (The other direction holds iff 𝐴 is nonempty, see r19.36zv 4530.) (Contributed by NM, 22-Oct-2003.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	rexlimivOLD 3191*	Obsolete version of rexlimiv 3154 as of 19-Dec-2024.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimivaOLD 3192*	Obsolete version of rexlimiva 3153 as of 23-Dec-2024. (Contributed by NM, 18-Dec-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimivwOLD 3193*	Obsolete version of rexlimivw 3157 as of 23-Dec-2024. (Contributed by FL, 19-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	r19.27v 3194*	Restricted quantitifer version of one direction of 19.27 2228. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.27zv 4529.) (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 3195*	Restricted quantifier version 19.41v 1949. Version of r19.41 3269 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 3196*	Restricted quantifier version of one direction of 19.28 2229. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.28zv 4524.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.42v 3197*	Restricted quantifier version of 19.42v 1953 (see also 19.42 2237). (Contributed by NM, 27-May-1998.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.32v 3198*	Restricted quantifier version of 19.32v 1939. (Contributed by NM, 25-Nov-2003.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.45v 3199*	Restricted quantifier version of one direction of 19.45 2239. The other direction holds when 𝐴 is nonempty, see r19.45zv 4526. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.44v 3200*	One direction of a restricted quantifier version of 19.44 2238. The other direction holds when 𝐴 is nonempty, see r19.44zv 4527. (Contributed by NM, 2-Apr-2004.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))