![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexbii | Unicode version |
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) |
Ref | Expression |
---|---|
ralbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexbidv 2321 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | trud 1251 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-rex 2306 |
This theorem is referenced by: 2rexbii 2327 r19.29r 2445 r19.42v 2461 rexcom13 2469 rexrot4 2470 3reeanv 2474 cbvrex2v 2536 rexcom4 2571 rexcom4a 2572 rexcom4b 2573 ceqsrex2v 2670 reu7 2730 0el 3235 iuncom 3654 iuncom4 3655 iuniin 3658 dfiunv2 3684 iunab 3694 iunin2 3711 iundif2ss 3713 iunun 3725 iunxiun 3727 iunpwss 3734 inuni 3900 iunopab 4009 sucel 4113 iunpw 4177 xpiundi 4341 xpiundir 4342 reliin 4402 rexxpf 4426 iunxpf 4427 cnvuni 4464 dmiun 4487 dfima3 4614 rniun 4677 dminxp 4708 imaco 4769 coiun 4773 isarep1 4928 rexrn 5247 ralrn 5248 elrnrexdmb 5250 fnasrn 5284 fnasrng 5286 rexima 5337 ralima 5338 abrexco 5341 imaiun 5342 fliftcnv 5378 abrexex2g 5689 abrexex2 5693 qsid 6107 eroveu 6133 genpdflem 6490 genpassl 6507 genpassu 6508 nqprm 6525 nqprrnd 6526 ltexprlemm 6574 ltexprlemopl 6575 ltexprlemopu 6577 elreal 6727 ublbneg 8324 4fvwrd4 8767 |
Copyright terms: Public domain | W3C validator |