Theorem ralbi 3100

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3058

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

This theorem depends on definitions:  df-bi 207  df-ral 3059

This theorem is referenced by:  rexbiOLD  3102  uniiunlem  4096  iineq2  5016  reusv2lem5  5407  ralrnmptw  7113  ralrnmpt  7115  f1mpt  7280  mpo2eqb  7564  ralrnmpo  7571  naddcom  8718  naddrid  8719  naddass  8732  rankonidlem  9865  acni2  10083  kmlem8  10195  kmlem13  10200  fimaxre3  12211  cau3lem  15389  rlim2  15528  rlim0  15540  rlim0lt  15541  catpropd  17753  funcres2b  17947  ulmss  26454  lgamgulmlem6  27091  colinearalg  28939  axpasch  28970  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  neibastop3  36344  bj-0int  37083  ralbi12f  38146  iineq12f  38150  pmapglbx  39751  ordelordALTVD  44864