Theorem ralbi 3121

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1851. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)

Assertion

Ref	Expression
ralbi	⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

Proof of Theorem ralbi

Step	Hyp	Ref	Expression
1		biimp 218	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3105	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 223	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3105	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 215	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  uniiunlem  4015  iineq2  4975  reusv2lem5  5368  ralrnmptw  7115  ralrnmpt  7117  f1mpt  7285  mpo2eqb  7572  ralrnmpo  7580  naddcom  8717  naddrid  8718  naddass  8731  rankonidlem  9862  acni2  10149  kmlem8  10260  kmlem13  10265  fimaxre3  12287  cau3lem  15548  rlim2  15689  rlim0  15701  rlim0lt  15702  catpropd  17909  funcres2b  18098  ulmss  26751  lgamgulmlem6  27388  colinearalg  29515  axpasch  29546  axcontlem2  29570  axcontlem4  29572  axcontlem7  29575  axcontlem8  29576  nmulrid  37123  neibastop3  37327  bj-0int  38212  ralbi12f  39283  iineq12f  39287  pmapglbx  41017  ordelordALTVD  46038