Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbi | Structured version Visualization version GIF version |
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1736. (Contributed by NM, 6-Oct-2003.) |
Ref | Expression |
---|---|
ralbi | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfra1 2925 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) | |
2 | rspa 2914 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | ralbida 2965 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ex 1696 df-nf 1701 df-ral 2901 |
This theorem is referenced by: uniiunlem 3653 iineq2 4474 reusv2lem5 4799 ralrnmpt 6276 f1mpt 6419 mpt22eqb 6667 ralrnmpt2 6673 rankonidlem 8574 acni2 8752 kmlem8 8862 kmlem13 8867 fimaxre3 10849 cau3lem 13942 rlim2 14075 rlim0 14087 rlim0lt 14088 catpropd 16192 funcres2b 16380 ulmss 23955 lgamgulmlem6 24560 colinearalg 25590 axpasch 25621 axcontlem2 25645 axcontlem4 25647 axcontlem7 25650 axcontlem8 25651 neibastop3 31527 ralbi12f 33139 iineq12f 33143 pmapglbx 34073 ordelordALTVD 38125 |
Copyright terms: Public domain | W3C validator |