Theorem ralbi 3120

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

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

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

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

This theorem is used by:  uniiunlem  4041  iineq2  4977  reusv2lem5  5373  ralrnmptw  7089  ralrnmpt  7091  f1mpt  7259  mpo2eqb  7542  ralrnmpo  7549  naddcom  8665  naddrid  8666  naddass  8679  rankonidlem  9796  acni2  10035  kmlem8  10146  kmlem13  10151  fimaxre3  12165  cau3lem  15411  rlim2  15552  rlim0  15564  rlim0lt  15565  catpropd  17769  funcres2b  17958  ulmss  26569  lgamgulmlem6  27207  colinearalg  29269  axpasch  29300  axcontlem2  29324  axcontlem4  29326  axcontlem7  29329  axcontlem8  29330  nmulrid  36697  neibastop3  36901  bj-0int  37771  ralbi12f  38837  iineq12f  38841  pmapglbx  40571  ordelordALTVD  45603