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 |
---|---|
ralbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2ralbii | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | ralbii 2963 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralbii 2963 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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 |
This theorem depends on definitions: df-bi 196 df-ral 2901 |
This theorem is referenced by: cnvso 5591 fununi 5878 dff14a 6427 isocnv2 6481 sorpss 6840 tpossym 7271 dford2 8400 isffth2 16399 ispos2 16771 issubm 17170 cntzrec 17589 oppgsubm 17615 opprirred 18525 opprsubrg 18624 gsummatr01lem3 20282 gsummatr01 20284 isbasis2g 20563 ist0-3 20959 isfbas2 21449 isclmp 22705 dfadj2 28128 adjval2 28134 cnlnadjeui 28320 adjbdln 28326 rmo4f 28721 isarchi 29067 iccllyscon 30486 dfso3 30856 elpotr 30930 dfon2 30941 f1opr 32689 isltrn2N 34424 fphpd 36398 isdomn3 36801 fiinfi 36897 ntrk1k3eqk13 37368 ordelordALT 37768 2reu4a 39838 issubmgm 41579 |
Copyright terms: Public domain | W3C validator |