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 1858 and albid 2214. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albidv | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1902 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1858 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 |
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 |
This theorem is referenced by: nfbidv 1914 2albidv 1915 sbjust 2059 sbequ 2081 sb6 2084 ax12wdemo 2130 sb4b 2492 sb4bOLD 2493 mojust 2614 mof 2640 eujust 2649 eujustALT 2650 eu6lem 2651 euf 2654 axextg 2792 axextmo 2794 eqeq1dALT 2821 nfceqdf 2969 drnfc1 2994 drnfc2 2996 ralbidv2 3192 ralxpxfr2d 3636 alexeqg 3641 pm13.183 3656 pm13.183OLD 3657 eqeu 3694 mo2icl 3702 euind 3712 reuind 3741 cdeqal 3757 sbcal 3830 sbcabel 3858 csbiebg 3912 ssconb 4111 reldisj 4398 sbcssg 4459 elint 4873 axrep1 5182 axreplem 5183 axrep2 5184 axrep4 5186 zfrepclf 5189 axsepg 5195 zfauscl 5196 bm1.3ii 5197 al0ssb 5203 eusv1 5282 euotd 5394 freq1 5518 frsn 5632 iota5 6331 sbcfung 6372 funimass4 6723 dffo3 6860 eufnfv 6982 dff13 7004 nfriotadw 7111 tfisi 7562 dfom2 7571 elom 7572 seqomlem2 8076 pssnn 8724 findcard 8745 findcard2 8746 findcard3 8749 fiint 8783 inf0 9072 axinf2 9091 tz9.1 9159 karden 9312 aceq0 9532 dfac5 9542 zfac 9870 brdom3 9938 axpowndlem3 10009 zfcndrep 10024 zfcndac 10029 elgch 10032 engch 10038 axgroth3 10241 axgroth4 10242 elnp 10397 elnpi 10398 infm3 11588 fz1sbc 12971 uzrdgfni 13314 trclfvcotr 14357 relexpindlem 14410 vdwmc2 16303 ramtlecl 16324 ramval 16332 ramub 16337 rami 16339 ramcl 16353 mreexexd 16907 mplsubglem 20142 mpllsslem 20143 istopg 21431 1stccn 21999 iskgen3 22085 fbfinnfr 22377 cnextfun 22600 metcld 23836 metcld2 23837 chlimi 28938 nmcexi 29730 disjxun0 30252 disjrdx 30269 funcnvmpt 30340 mclsssvlem 32706 mclsval 32707 mclsind 32714 elintfv 32904 dfon2lem6 32930 dfon2lem7 32931 dfon2lem8 32932 dfon2 32934 sscoid 33271 trer 33561 bj-ssblem1 33884 bj-ax12 33887 mobidvALT 34078 bj-sbceqgALT 34116 bj-nuliota 34244 bj-bm1.3ii 34251 wl-mo2t 34692 wl-dfralf 34720 isass 35005 releccnveq 35400 ecin0 35487 inecmo 35490 alrmomodm 35494 extssr 35629 eltrrels3 35696 eleqvrels3 35708 axc11n-16 35954 cdlemefrs29bpre0 37412 elmapintab 39834 cnvcnvintabd 39838 iunrelexpuztr 39942 ntrneiiso 40319 ntrneik2 40320 ntrneix2 40321 ntrneikb 40322 mnuop123d 40475 pm14.122b 40632 iotavalb 40639 trsbc 40751 dffo3f 41314 eusnsn 43138 aiota0def 43171 setrecseq 44716 setrec1lem1 44718 setrec2fun 44723 setrec2lem2 44725 |
Copyright terms: Public domain | W3C validator |