Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbidv | GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) |
Ref | Expression |
---|---|
ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1461 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | ralbid 2366 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∀wral 2348 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-4 1440 ax-17 1459 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-ral 2353 |
This theorem is referenced by: ralbii 2372 2ralbidv 2390 rexralbidv 2392 r19.32vdc 2503 raleqbi1dv 2557 raleqbidv 2561 cbvral2v 2585 rspc2 2711 rspc3v 2716 reu6i 2783 reu7 2787 sbcralt 2890 sbcralg 2892 raaanlem 3346 2ralunsn 3590 elintg 3644 elintrabg 3649 eliin 3683 bnd2 3947 poeq1 4054 soeq1 4070 frforeq1 4098 frforeq3 4102 frirrg 4105 frind 4107 weeq1 4111 reusv3 4210 ontr2exmid 4268 reg2exmidlema 4277 posng 4430 ralxpf 4500 cnvpom 4880 funcnvuni 4988 dff4im 5334 dff13f 5430 eusvobj2 5518 ofreq 5735 smoeq 5928 recseq 5944 tfr0 5960 tfrlemiex 5968 nneneq 6343 ac6sfi 6379 supeq1 6399 supeq3 6403 supmoti 6406 eqsupti 6409 supubti 6412 suplubti 6413 supisoex 6422 cnvinfex 6431 eqinfti 6433 infvalti 6435 elinp 6664 prloc 6681 cauappcvgprlemladdru 6846 cauappcvgprlemladdrl 6847 caucvgpr 6872 caucvgprpr 6902 caucvgsrlemgt1 6971 caucvgsrlemoffres 6976 caucvgsr 6978 axcaucvglemcau 7064 axcaucvglemres 7065 lbreu 8023 nnsub 8077 indstr 8681 supinfneg 8683 infsupneg 8684 ublbneg 8698 lbzbi 8701 iccsupr 8989 bccl 9694 cau4 10002 caubnd2 10003 maxleast 10099 rexanre 10106 rexico 10107 fimaxre2 10109 minmax 10112 clim 10120 clim2 10122 clim2c 10123 clim0c 10125 climabs0 10146 cn1lem 10152 zsupcllemstep 10341 infssuzex 10345 bezoutlemstep 10386 bezoutlemmain 10387 bezoutlemex 10390 bezoutlemeu 10396 dfgcd3 10399 bezout 10400 dfgcd2 10403 sqrt2irr 10541 bj-omtrans 10751 |
Copyright terms: Public domain | W3C validator |