Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2ralbidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
2ralbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 468 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | ralbidva 3193 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralbidva 3193 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ral 3140 |
This theorem is referenced by: disjxun 5055 reu3op 6136 opreu2reurex 6138 isocnv3 7074 isotr 7078 f1oweALT 7662 fnmpoovd 7771 tosso 17634 pospropd 17732 isipodrs 17759 mndpropd 17924 mhmpropd 17950 efgred 18803 cmnpropd 18845 ringpropd 19261 lmodprop2d 19625 lsspropd 19718 islmhm2 19739 lmhmpropd 19774 assapropd 20029 islindf4 20910 scmatmats 21048 cpmatel2 21249 1elcpmat 21251 m2cpminvid2 21291 decpmataa0 21304 pmatcollpw2lem 21313 connsub 21957 hausdiag 22181 ist0-4 22265 ismet2 22870 txmetcnp 23084 txmetcn 23085 metuel2 23102 metucn 23108 isngp3 23134 nlmvscn 23223 isclmp 23628 isncvsngp 23680 ipcn 23776 iscfil2 23796 caucfil 23813 cfilresi 23825 ulmdvlem3 24917 cxpcn3 25256 tgjustf 26186 tgjustr 26187 tgcgr4 26244 perpcom 26426 brbtwn2 26618 colinearalglem2 26620 eengtrkg 26699 isarchi2 30741 elmrsubrn 32664 isbnd3b 34944 iscvlat2N 36340 ishlat3N 36370 gicabl 39577 isdomn3 39682 mgmpropd 43919 mgmhmpropd 43929 lidlmmgm 44124 lindslinindsimp2 44446 |
Copyright terms: Public domain | W3C validator |