Theorem ralrn 7035

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6850	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6895	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2744	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3084	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5356	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3061  Vcvv 3441  ran crn 5626   Fn wfn 6488  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-fv 6501

This theorem is referenced by:  ralrnmptw  7041  ralrnmpt  7043  cbvfo  7237  isoselem  7289  indexfi  9264  ordtypelem9  9435  ordtypelem10  9436  wemapwe  9610  numacn  9963  acndom  9965  rpnnen1lem3  12896  fsequb2  13903  limsuple  15405  limsupval2  15407  climsup  15597  ruclem11  16169  ruclem12  16170  prmreclem6  16853  imasaddfnlem  17453  imasvscafn  17462  cycsubgcl  19139  ghmrn  19162  ghmnsgima  19173  pgpssslw  19547  gexex  19786  dprdfcntz  19950  znf1o  21510  frlmlbs  21756  lindfrn  21780  ptcnplem  23569  kqt0lem  23684  isr0  23685  regr1lem2  23688  uzrest  23845  tmdgsum2  24044  imasf1oxmet  24323  imasf1omet  24324  bndth  24917  evth  24918  ovolficcss  25430  ovollb2lem  25449  ovolunlem1  25458  ovoliunlem1  25463  ovoliunlem2  25464  ovoliun2  25467  ovolscalem1  25474  ovolicc1  25477  voliunlem2  25512  voliunlem3  25513  ioombl1lem4  25522  uniioovol  25540  uniioombllem2  25544  uniioombllem3  25546  uniioombllem6  25549  volsup2  25566  vitalilem3  25571  mbfsup  25625  mbfinf  25626  mbflimsup  25627  itg1ge0  25647  itg1mulc  25665  itg1climres  25675  mbfi1fseqlem4  25679  itg2seq  25703  itg2monolem1  25711  itg2mono  25714  itg2i1fseq2  25717  itg2gt0  25721  itg2cnlem1  25722  itg2cn  25724  limciun  25855  plycpn  26257  hmopidmchi  32230  hmopidmpji  32231  rge0scvg  34108  mclsax  35765  mblfinlem2  37861  ismtyhmeolem  38007  nacsfix  43021  fnwe2lem2  43360  gneispace  44442  climinf  45919  liminfval2  46079