![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralbidva | GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1539 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | ralbida 2484 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: raleqbidva 2700 poinxp 4713 funimass4 5587 fnmptfvd 5641 funimass3 5653 funconstss 5655 cocan1 5809 cocan2 5810 isocnv2 5834 isores2 5835 isoini2 5841 ofrfval 6116 ofrfval2 6124 dfsmo2 6313 smores 6318 smores2 6320 ac6sfi 6927 supisolem 7038 ordiso2 7065 ismkvnex 7184 nninfwlporlemd 7201 caucvgsrlemcau 7823 suplocsrlempr 7837 axsuploc 8061 suprleubex 8942 dfinfre 8944 zextlt 9376 prime 9383 infregelbex 9630 fzshftral 10140 fimaxq 10842 clim 11324 clim2 11326 clim2c 11327 clim0c 11329 climabs0 11350 climrecvg1n 11391 mertenslem2 11579 mertensabs 11580 dfgcd2 12050 sqrt2irr 12197 pc11 12366 pcz 12367 1arith 12402 infpn2 12510 grpidpropdg 12853 sgrppropd 12891 mndpropd 12916 grppropd 12977 issubg4m 13149 rngpropd 13326 ringpropd 13409 oppr1g 13449 lsspropdg 13764 isridlrng 13815 isridl 13836 tgss2 14056 neipsm 14131 ssidcn 14187 lmbrf 14192 cnnei 14209 cnrest2 14213 lmss 14223 lmres 14225 ismet2 14331 elmopn2 14426 metss 14471 metrest 14483 metcnp 14489 metcnp2 14490 metcn 14491 txmetcnp 14495 divcnap 14532 elcncf2 14538 mulc1cncf 14553 cncfmet 14556 cdivcncfap 14564 limcdifap 14608 limcmpted 14609 cnlimc 14618 2sqlem6 14945 iswomni0 15278 cndcap 15286 |
Copyright terms: Public domain | W3C validator |