| 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 1866 and albid 2222. (Contributed by NM, 26-May-1993.) |
| Ref | Expression |
|---|---|
| albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| albidv | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 1910 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 3 | 1, 2 | albidh 1866 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: nfbidv 1922 2albidv 1923 sbjust 2063 sbequ 2083 sb6 2085 ax12wdemo 2135 sb4b 2480 mojust 2539 mof 2563 eujust 2571 eujustALT 2572 eu6lem 2573 euf 2576 axextg 2710 axextmo 2712 eqeq1dALT 2740 nfceqdf 2901 drnfc1 2925 drnfc2 2926 ralbidv2 3174 ralxpxfr2d 3646 alexeqg 3651 pm13.183 3666 elab6g 3669 elabd2 3670 eqeu 3712 mo2icl 3720 euind 3730 reuind 3759 cdeqal 3775 sbcal 3849 sbccomlem 3869 sbcabel 3878 csbiebg 3931 ssconb 4142 reldisj 4453 sbcssg 4520 elint 4952 axrep1 5280 axreplem 5281 axrep2 5282 axrep4OLD 5286 zfrepclf 5291 axsepg 5297 zfauscl 5298 bm1.3iiOLD 5302 al0ssb 5308 eusv1 5391 euotd 5518 freq1 5652 frsn 5773 iota5 6544 dffun2 6571 sbcfung 6590 funimass4 6973 dffo3 7122 dffo3f 7126 eufnfv 7249 dff13 7275 fnssintima 7382 nfriotadw 7396 imaeqalov 7672 tfisi 7880 dfom2 7889 elom 7890 xpord3inddlem 8179 seqomlem2 8491 findcard 9203 findcard2 9204 pssnn 9208 ssfi 9213 findcard3 9318 findcard3OLD 9319 fiint 9366 fiintOLD 9367 inf0 9661 axinf2 9680 ttrclss 9760 ttrclselem2 9766 tz9.1 9769 karden 9935 aceq0 10158 dfac5 10169 zfac 10500 brdom3 10568 axpowndlem3 10639 zfcndrep 10654 zfcndac 10659 elgch 10662 engch 10668 axgroth3 10871 axgroth4 10872 elnp 11027 elnpi 11028 infm3 12227 fz1sbc 13640 uzrdgfni 13999 trclfvcotr 15048 relexpindlem 15102 vdwmc2 17017 ramtlecl 17038 ramval 17046 ramub 17051 rami 17053 ramcl 17067 mreexexd 17691 mplsubglem 22019 mpllsslem 22020 ismhp3 22146 istopg 22901 1stccn 23471 iskgen3 23557 fbfinnfr 23849 cnextfun 24072 metcld 25340 metcld2 25341 noseqrdgfn 28312 chlimi 31253 nmcexi 32045 disjxun0 32587 disjrdx 32604 funcnvmpt 32677 mclsssvlem 35567 mclsval 35568 mclsind 35575 elintfv 35765 dfon2lem6 35789 dfon2lem7 35790 dfon2lem8 35791 dfon2 35793 sscoid 35914 sbequbidv 36215 disjeq12dv 36216 ixpeq12dv 36217 cbvsbdavw 36255 cbvsbdavw2 36256 cbvdisjdavw 36269 cbvdisjdavw2 36290 trer 36317 bj-ssblem1 36655 bj-ax12 36658 mobidvALT 36858 bj-sbceqgALT 36903 bj-nuliota 37058 bj-bm1.3ii 37065 wl-ax12v2cl 37507 wl-mo2t 37576 isass 37853 releccnveq 38259 ecin0 38353 inecmo 38356 alrmomodm 38360 extssr 38510 eltrrels3 38581 eleqvrels3 38594 axc11n-16 38939 cdlemefrs29bpre0 40398 eu6w 42686 unielss 43230 orddif0suc 43281 elmapintab 43609 cnvcnvintabd 43613 iunrelexpuztr 43732 ntrneiiso 44104 ntrneik2 44105 ntrneix2 44106 ntrneikb 44107 mnuop123d 44281 pm14.122b 44442 iotavalb 44449 trsbc 44560 eusnsn 47038 aiota0def 47108 ichbidv 47440 mof0 48747 eufsnlem 48750 setrecseq 49204 setrec1lem1 49206 setrec2fun 49211 setrec2lem2 49213 |
| Copyright terms: Public domain | W3C validator |