Theorem ralbi 3092

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1812. (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 214	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3074	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 219	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3074	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803

This theorem depends on definitions:  df-bi 206  df-ral 3051

This theorem is referenced by:  rexbiOLD  3094  uniiunlem  4080  iineq2  5017  reusv2lem5  5402  ralrnmptw  7103  ralrnmpt  7105  f1mpt  7271  mpo2eqb  7553  ralrnmpo  7560  naddcom  8703  naddrid  8704  naddass  8717  rankonidlem  9858  acni2  10076  kmlem8  10187  kmlem13  10192  fimaxre3  12198  cau3lem  15342  rlim2  15481  rlim0  15493  rlim0lt  15494  catpropd  17697  funcres2b  17891  ulmss  26383  lgamgulmlem6  27016  colinearalg  28798  axpasch  28829  axcontlem2  28853  axcontlem4  28855  axcontlem7  28858  axcontlem8  28859  neibastop3  35979  bj-0int  36713  ralbi12f  37766  iineq12f  37770  pmapglbx  39374  ordelordALTVD  44450