| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 2ralbii | Structured version Visualization version GIF version | ||
| Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
| Ref | Expression |
|---|---|
| 2ralbii.1 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| 2ralbii | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2ralbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) |
| 3 | 2 | ralbii 3093 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: 3ralbii 3130 ralnex3 3134 rmo4f 3741 2reu4lem 4522 cnvso 6308 fununi 6641 dff14a 7290 isocnv2 7351 f1opr 7489 sorpss 7748 xpord3inddlem 8179 tpossym 8283 dford2 9660 isffth2 17963 ispos2 18361 issubmgm 18715 issubm 18816 cntzrec 19354 oppgsubm 19381 opprirred 20422 opprsubrng 20559 rhmimasubrng 20566 cntzsubrng 20567 opprsubrg 20593 isdomn5 20710 isdomn3 20715 gsummatr01lem3 22663 gsummatr01 22665 isbasis2g 22955 ist0-3 23353 isfbas2 23843 isclmp 25130 addsproplem4 28005 addsproplem6 28007 addsprop 28009 negsproplem4 28063 negsproplem6 28065 negsprop 28067 mulsprop 28156 dfadj2 31904 adjval2 31910 cnlnadjeui 32096 adjbdln 32102 isarchi 33189 prmidl0 33478 ply1dg3rt0irred 33607 dff15 35098 iccllysconn 35255 dfso3 35720 elpotr 35782 dfon2 35793 idinxpss 38313 inxpssidinxp 38317 idinxpssinxp 38318 dfeldisj5 38722 isltrn2N 40122 hashnexinj 42129 fphpd 42827 fiinfi 43586 ntrk1k3eqk13 44063 ordelordALT 44557 dfac5prim 45007 disjinfi 45197 isthinc2 49070 isthinc3 49071 |
| Copyright terms: Public domain | W3C validator |