Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ac6num Structured version   Visualization version   GIF version

Theorem ac6num 9893
 Description: A version of ac6 9894 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
ac6num.1 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
Assertion
Ref Expression
ac6num ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Distinct variable groups:   𝑥,𝑓,𝐴   𝑦,𝑓,𝐵,𝑥   𝜑,𝑓   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑓)   𝐴(𝑦)   𝑉(𝑥,𝑦,𝑓)

Proof of Theorem ac6num
Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4944 . . . . . . . . 9 𝑥 𝑥𝐴 {𝑦𝐵𝜑}
21nfel1 2992 . . . . . . . 8 𝑥 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card
3 ssiun2 4962 . . . . . . . . 9 (𝑥𝐴 → {𝑦𝐵𝜑} ⊆ 𝑥𝐴 {𝑦𝐵𝜑})
4 ssexg 5218 . . . . . . . . . 10 (({𝑦𝐵𝜑} ⊆ 𝑥𝐴 {𝑦𝐵𝜑} ∧ 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card) → {𝑦𝐵𝜑} ∈ V)
54expcom 416 . . . . . . . . 9 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → ({𝑦𝐵𝜑} ⊆ 𝑥𝐴 {𝑦𝐵𝜑} → {𝑦𝐵𝜑} ∈ V))
63, 5syl5 34 . . . . . . . 8 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → (𝑥𝐴 → {𝑦𝐵𝜑} ∈ V))
72, 6ralrimi 3214 . . . . . . 7 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → ∀𝑥𝐴 {𝑦𝐵𝜑} ∈ V)
8 dfiun2g 4946 . . . . . . 7 (∀𝑥𝐴 {𝑦𝐵𝜑} ∈ V → 𝑥𝐴 {𝑦𝐵𝜑} = {𝑧 ∣ ∃𝑥𝐴 𝑧 = {𝑦𝐵𝜑}})
97, 8syl 17 . . . . . 6 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → 𝑥𝐴 {𝑦𝐵𝜑} = {𝑧 ∣ ∃𝑥𝐴 𝑧 = {𝑦𝐵𝜑}})
10 eqid 2819 . . . . . . . 8 (𝑥𝐴 ↦ {𝑦𝐵𝜑}) = (𝑥𝐴 ↦ {𝑦𝐵𝜑})
1110rnmpt 5820 . . . . . . 7 ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = {𝑦𝐵𝜑}}
1211unieqi 4839 . . . . . 6 ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = {𝑦𝐵𝜑}}
139, 12syl6eqr 2872 . . . . 5 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → 𝑥𝐴 {𝑦𝐵𝜑} = ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}))
14 id 22 . . . . 5 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card)
1513, 14eqeltrrd 2912 . . . 4 ( 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card → ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∈ dom card)
16153ad2ant2 1128 . . 3 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∈ dom card)
17 simp3 1132 . . . . 5 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∀𝑥𝐴𝑦𝐵 𝜑)
18 necom 3067 . . . . . . . 8 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∅ ≠ {𝑦𝐵𝜑})
19 rabn0 4337 . . . . . . . 8 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∃𝑦𝐵 𝜑)
20 df-ne 3015 . . . . . . . 8 (∅ ≠ {𝑦𝐵𝜑} ↔ ¬ ∅ = {𝑦𝐵𝜑})
2118, 19, 203bitr3i 303 . . . . . . 7 (∃𝑦𝐵 𝜑 ↔ ¬ ∅ = {𝑦𝐵𝜑})
2221ralbii 3163 . . . . . 6 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴 ¬ ∅ = {𝑦𝐵𝜑})
23 ralnex 3234 . . . . . 6 (∀𝑥𝐴 ¬ ∅ = {𝑦𝐵𝜑} ↔ ¬ ∃𝑥𝐴 ∅ = {𝑦𝐵𝜑})
2422, 23bitri 277 . . . . 5 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ¬ ∃𝑥𝐴 ∅ = {𝑦𝐵𝜑})
2517, 24sylib 220 . . . 4 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ¬ ∃𝑥𝐴 ∅ = {𝑦𝐵𝜑})
26 0ex 5202 . . . . 5 ∅ ∈ V
2710elrnmpt 5821 . . . . 5 (∅ ∈ V → (∅ ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ↔ ∃𝑥𝐴 ∅ = {𝑦𝐵𝜑}))
2826, 27ax-mp 5 . . . 4 (∅ ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ↔ ∃𝑥𝐴 ∅ = {𝑦𝐵𝜑})
2925, 28sylnibr 331 . . 3 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ¬ ∅ ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}))
30 ac5num 9454 . . 3 (( ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∈ dom card ∧ ¬ ∅ ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})) → ∃𝑔(𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧))
3116, 29, 30syl2anc 586 . 2 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑔(𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧))
32 ffn 6507 . . . . . 6 (𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) → 𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}))
3332anim1i 616 . . . . 5 ((𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧) → (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧))
3473ad2ant2 1128 . . . . . . 7 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∀𝑥𝐴 {𝑦𝐵𝜑} ∈ V)
35 fveq2 6663 . . . . . . . . 9 (𝑧 = {𝑦𝐵𝜑} → (𝑔𝑧) = (𝑔‘{𝑦𝐵𝜑}))
36 id 22 . . . . . . . . 9 (𝑧 = {𝑦𝐵𝜑} → 𝑧 = {𝑦𝐵𝜑})
3735, 36eleq12d 2905 . . . . . . . 8 (𝑧 = {𝑦𝐵𝜑} → ((𝑔𝑧) ∈ 𝑧 ↔ (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑}))
3810, 37ralrnmptw 6853 . . . . . . 7 (∀𝑥𝐴 {𝑦𝐵𝜑} ∈ V → (∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧 ↔ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑}))
3934, 38syl 17 . . . . . 6 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → (∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧 ↔ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑}))
4039anbi2d 630 . . . . 5 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ((𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧) ↔ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})))
4133, 40syl5ib 246 . . . 4 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ((𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧) → (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})))
42 simpl1 1185 . . . . . . 7 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → 𝐴𝑉)
4342mptexd 6979 . . . . . 6 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) ∈ V)
44 ssrab2 4054 . . . . . . . . . . 11 {𝑦𝐵𝜑} ⊆ 𝐵
4544sseli 3961 . . . . . . . . . 10 ((𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑} → (𝑔‘{𝑦𝐵𝜑}) ∈ 𝐵)
4645ralimi 3158 . . . . . . . . 9 (∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑} → ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ 𝐵)
4746ad2antll 727 . . . . . . . 8 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ 𝐵)
48 eqid 2819 . . . . . . . . 9 (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))
4948fmpt 6867 . . . . . . . 8 (∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ 𝐵 ↔ (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})):𝐴𝐵)
5047, 49sylib 220 . . . . . . 7 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})):𝐴𝐵)
51 nfcv 2975 . . . . . . . . . . 11 𝑦𝐵
5251elrabsf 3814 . . . . . . . . . 10 ((𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑} ↔ ((𝑔‘{𝑦𝐵𝜑}) ∈ 𝐵[(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑))
5352simprbi 499 . . . . . . . . 9 ((𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑} → [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑)
5453ralimi 3158 . . . . . . . 8 (∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑} → ∀𝑥𝐴 [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑)
5554ad2antll 727 . . . . . . 7 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → ∀𝑥𝐴 [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑)
5650, 55jca 514 . . . . . 6 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → ((𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})):𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑))
57 feq1 6488 . . . . . . 7 (𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) → (𝑓:𝐴𝐵 ↔ (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})):𝐴𝐵))
58 nfmpt1 5155 . . . . . . . . 9 𝑥(𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))
5958nfeq2 2993 . . . . . . . 8 𝑥 𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))
60 fvex 6676 . . . . . . . . . 10 (𝑓𝑥) ∈ V
61 ac6num.1 . . . . . . . . . 10 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
6260, 61sbcie 3810 . . . . . . . . 9 ([(𝑓𝑥) / 𝑦]𝜑𝜓)
63 fveq1 6662 . . . . . . . . . . 11 (𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) → (𝑓𝑥) = ((𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))‘𝑥))
64 fvex 6676 . . . . . . . . . . . 12 (𝑔‘{𝑦𝐵𝜑}) ∈ V
6548fvmpt2 6772 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ (𝑔‘{𝑦𝐵𝜑}) ∈ V) → ((𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))‘𝑥) = (𝑔‘{𝑦𝐵𝜑}))
6664, 65mpan2 689 . . . . . . . . . . 11 (𝑥𝐴 → ((𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑}))‘𝑥) = (𝑔‘{𝑦𝐵𝜑}))
6763, 66sylan9eq 2874 . . . . . . . . . 10 ((𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) ∧ 𝑥𝐴) → (𝑓𝑥) = (𝑔‘{𝑦𝐵𝜑}))
6867sbceq1d 3775 . . . . . . . . 9 ((𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) ∧ 𝑥𝐴) → ([(𝑓𝑥) / 𝑦]𝜑[(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑))
6962, 68syl5bbr 287 . . . . . . . 8 ((𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) ∧ 𝑥𝐴) → (𝜓[(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑))
7059, 69ralbida 3228 . . . . . . 7 (𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑))
7157, 70anbi12d 632 . . . . . 6 (𝑓 = (𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})) → ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓) ↔ ((𝑥𝐴 ↦ (𝑔‘{𝑦𝐵𝜑})):𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑔‘{𝑦𝐵𝜑}) / 𝑦]𝜑)))
7243, 56, 71spcedv 3597 . . . . 5 (((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) ∧ (𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑})) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
7372ex 415 . . . 4 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ((𝑔 Fn ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑥𝐴 (𝑔‘{𝑦𝐵𝜑}) ∈ {𝑦𝐵𝜑}) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
7441, 73syld 47 . . 3 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ((𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
7574exlimdv 1927 . 2 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → (∃𝑔(𝑔:ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})⟶ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑}) ∧ ∀𝑧 ∈ ran (𝑥𝐴 ↦ {𝑦𝐵𝜑})(𝑔𝑧) ∈ 𝑧) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
7631, 75mpd 15 1 ((𝐴𝑉 𝑥𝐴 {𝑦𝐵𝜑} ∈ dom card ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1081   = wceq 1530  ∃wex 1773   ∈ wcel 2107  {cab 2797   ≠ wne 3014  ∀wral 3136  ∃wrex 3137  {crab 3140  Vcvv 3493  [wsbc 3770   ⊆ wss 3934  ∅c0 4289  ∪ cuni 4830  ∪ ciun 4910   ↦ cmpt 5137  dom cdm 5548  ran crn 5549   Fn wfn 6343  ⟶wf 6344  ‘cfv 6348  cardccrd 9356 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-en 8502  df-card 9360 This theorem is referenced by:  ac6  9894  ptcmplem3  22654  poimirlem32  34911
 Copyright terms: Public domain W3C validator