![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > albidv | Structured version Visualization version GIF version |
Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1861 and albid 2210. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albidv | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1905 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1861 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: nfbidv 1917 2albidv 1918 sbjust 2058 sbequ 2078 sb6 2080 ax12wdemo 2123 sb4b 2468 mojust 2527 mof 2551 eujust 2559 eujustALT 2560 eu6lem 2561 euf 2564 axextg 2698 axextmo 2700 eqeq1dALT 2728 nfceqdf 2886 nfceqdfOLD 2887 drnfc1 2911 drnfc1OLD 2912 drnfc2 2913 drnfc2OLD 2914 ralbidv2 3163 ralxpxfr2d 3629 alexeqg 3634 pm13.183 3651 elab6g 3654 elabd2 3655 eqeu 3698 mo2icl 3706 euind 3716 reuind 3745 cdeqal 3761 sbcal 3837 sbcabel 3868 csbiebg 3922 ssconb 4134 reldisj 4453 reldisjOLD 4454 sbcssg 4525 elint 4956 axrep1 5287 axreplem 5288 axrep2 5289 axrep4 5291 zfrepclf 5295 axsepg 5301 zfauscl 5302 bm1.3ii 5303 al0ssb 5309 eusv1 5391 euotd 5515 freq1 5648 frsn 5765 iota5 6532 dffun2 6559 sbcfung 6578 funimass4 6962 dffo3 7111 dffo3f 7115 eufnfv 7241 dff13 7265 fnssintima 7369 nfriotadw 7383 imaeqalov 7660 tfisi 7864 dfom2 7873 elom 7874 xpord3inddlem 8159 seqomlem2 8472 findcard 9188 findcard2 9189 pssnn 9193 ssfi 9198 pssnnOLD 9290 findcard2OLD 9309 findcard3 9310 findcard3OLD 9311 fiint 9350 inf0 9646 axinf2 9665 ttrclss 9745 ttrclselem2 9751 tz9.1 9754 karden 9920 aceq0 10143 dfac5 10153 zfac 10485 brdom3 10553 axpowndlem3 10624 zfcndrep 10639 zfcndac 10644 elgch 10647 engch 10653 axgroth3 10856 axgroth4 10857 elnp 11012 elnpi 11013 infm3 12206 fz1sbc 13612 uzrdgfni 13959 trclfvcotr 14992 relexpindlem 15046 vdwmc2 16951 ramtlecl 16972 ramval 16980 ramub 16985 rami 16987 ramcl 17001 mreexexd 17631 mplsubglem 21961 mpllsslem 21962 ismhp3 22090 istopg 22841 1stccn 23411 iskgen3 23497 fbfinnfr 23789 cnextfun 24012 metcld 25278 metcld2 25279 noseqrdgfn 28229 chlimi 31116 nmcexi 31908 disjxun0 32443 disjrdx 32460 funcnvmpt 32534 mclsssvlem 35303 mclsval 35304 mclsind 35311 elintfv 35491 dfon2lem6 35515 dfon2lem7 35516 dfon2lem8 35517 dfon2 35519 sscoid 35640 trer 35931 bj-ssblem1 36261 bj-ax12 36264 mobidvALT 36465 bj-sbceqgALT 36511 bj-nuliota 36667 bj-bm1.3ii 36674 wl-mo2t 37173 isass 37450 releccnveq 37860 ecin0 37954 inecmo 37957 alrmomodm 37961 extssr 38111 eltrrels3 38182 eleqvrels3 38195 axc11n-16 38540 cdlemefrs29bpre0 39999 eu6w 42236 unielss 42788 orddif0suc 42839 elmapintab 43168 cnvcnvintabd 43172 iunrelexpuztr 43291 ntrneiiso 43663 ntrneik2 43664 ntrneix2 43665 ntrneikb 43666 mnuop123d 43841 pm14.122b 44002 iotavalb 44009 trsbc 44121 eusnsn 46546 aiota0def 46614 ichbidv 46930 mof0 48076 eufsnlem 48079 setrecseq 48302 setrec1lem1 48304 setrec2fun 48309 setrec2lem2 48311 |
Copyright terms: Public domain | W3C validator |