![]() |
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). (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albidv | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1953 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1911 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 |
This theorem is referenced by: nfbidv 1965 2albidv 1966 ax12wdemo 2129 mojust 2550 mof 2578 mofOLD 2579 eujust 2589 eujustALT 2590 eu6lem 2591 eu6OLD 2594 euf 2595 eufOLD 2596 eubidvOLD 2620 axext3 2756 axext3ALT 2757 axextmo 2759 bm1.1OLD 2760 eqeq1dALT 2781 nfceqdf 2930 drnfc1 2951 drnfc2 2953 ralbidv2 3166 ralxpxfr2d 3530 alexeqg 3535 pm13.183 3549 pm13.183OLD 3550 eqeu 3587 mo2icl 3597 euind 3605 reuind 3628 cdeqal 3641 sbcal 3707 sbcabel 3734 csbiebg 3774 ssconb 3966 reldisj 4245 sbcssg 4306 elint 4716 axrep1 5007 axreplem 5008 axrep2 5009 axrep4 5011 zfrepclf 5013 axsep2 5018 zfauscl 5019 bm1.3ii 5020 al0ssb 5027 eusv1 5103 euotd 5210 freq1 5325 frsn 5437 iota5 6119 sbcfung 6159 funimass4 6507 dffo3 6638 eufnfv 6763 dff13 6784 tfisi 7336 dfom2 7345 elom 7346 seqomlem2 7829 pssnn 8466 findcard 8487 findcard2 8488 findcard3 8491 fiint 8525 inf0 8815 axinf2 8834 tz9.1 8902 karden 9055 aceq0 9274 dfac5 9284 zfac 9617 brdom3 9685 axpowndlem3 9756 zfcndrep 9771 zfcndac 9776 elgch 9779 engch 9785 axgroth3 9988 axgroth4 9989 elnp 10144 elnpi 10145 infm3 11336 fz1sbc 12734 uzrdgfni 13076 trclfvcotr 14157 relexpindlem 14210 vdwmc2 16087 ramtlecl 16108 ramval 16116 ramub 16121 rami 16123 ramcl 16137 mreexexd 16694 mplsubglem 19831 mpllsslem 19832 istopg 21107 1stccn 21675 iskgen3 21761 fbfinnfr 22053 cnextfun 22276 metcld 23512 metcld2 23513 chlimi 28663 nmcexi 29457 disjrdx 29967 funcnvmpt 30032 mclsssvlem 32058 mclsval 32059 mclsind 32066 elintfv 32255 dfon2lem6 32281 dfon2lem7 32282 dfon2lem8 32283 dfon2 32285 sscoid 32609 trer 32899 bj-ssbjustlem 33208 bj-ssbequ 33220 bj-ssblem1 33221 bj-axext3 33346 bj-axrep1 33365 bj-axrep2 33366 bj-axrep3 33367 bj-axrep4 33368 mobidvALT 33414 bj-sbceqgALT 33468 bj-axsep2 33494 bj-nuliota 33591 bj-bm1.3ii 33596 wl-mo2t 33951 wl-dfralf 33976 isass 34269 releccnveq 34657 ecin0 34745 inecmo 34748 alrmomodm 34752 extssr 34887 eltrrels3 34954 eleqvrels3 34965 axc11n-16 35092 cdlemefrs29bpre0 36550 elmapintab 38859 cnvcnvintabd 38863 iunrelexpuztr 38968 ntrneiiso 39345 ntrneik2 39346 ntrneix2 39347 ntrneikb 39348 pm14.122b 39579 iotavalb 39586 trsbc 39700 dffo3f 40287 eusnsn 42095 aiota0def 42124 fun2dmnopgexmpl 42325 setrecseq 43537 setrec1lem1 43539 setrec2fun 43544 setrec2lem2 43546 |
Copyright terms: Public domain | W3C validator |